{-# 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TargetDependencies
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec Config
cfg LocalVars
localVars LogicNameEnv
lnameEnv LogicMap
lmap TargetSrc
targetSrc Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec TargetDependencies
dependencies = do
  let targDiagnostics :: Either Diagnostics ()
targDiagnostics     = Config
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TargetSrc
-> Either Diagnostics ()
Bare.checkTargetSrc Config
cfg Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec TargetSrc
targetSrc
  let depsDiagnostics :: Either Diagnostics [()]
depsDiagnostics     = ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Either Diagnostics ())
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either Diagnostics ()
Bare.checkBareSpec (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> Either Diagnostics ())
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Either Diagnostics ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd) [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
legacyDependencies
  let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either Diagnostics ()
Bare.checkBareSpec Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec
  let stratDiagnostics :: Either Diagnostics [Name]
stratDiagnostics   = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TargetSrc -> Either Diagnostics [Name]
Bare.checkStratTys Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec TargetSrc
targetSrc
  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 Either Diagnostics ()
-> Either Diagnostics [Name] -> Either Diagnostics [Name]
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 [Name]
stratDiagnostics of
   Left Diagnostics
d | Diagnostics -> Bool
noErrors Diagnostics
d -> [Name]
-> [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 [Name]
stratNames   -> [Name]
-> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Name]
stratNames [Warning]
forall a. Monoid a => a
mempty
  where
    secondPhase :: [Ghc.Name] -> [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
    secondPhase :: [Name]
-> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Name]
stratNames [Warning]
phaseOneWarns = do
      diagOrSpec <- [Name]
-> Config
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec [Name]
stratNames Config
cfg LogicNameEnv
lnameEnv LocalVars
localVars (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
fromBareSpecLHName (BareSpecLHName
 -> Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> BareSpecLHName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> BareSpecLHName
unsafeFromLiftedSpec LiftedSpec
ls)

    legacyDependencies :: [(ModName, BareSpec)]
    legacyDependencies :: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> ModName)
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> ModName
forall a b. (a, b) -> a
fst ([(ModName,
   Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
 -> [(ModName,
      Spec
        Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a b. (a -> b) -> a -> b
$ ((StableModule, LiftedSpec)
 -> (ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
-> [(StableModule, LiftedSpec)]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a b. (a -> b) -> [a] -> [b]
map (StableModule, LiftedSpec)
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
toLegacyDep ([(StableModule, LiftedSpec)]
 -> [(ModName,
      Spec
        Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])
-> [(StableModule, LiftedSpec)]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> BareSpecLHName
toBareSpecLHName Config
cfg LogicNameEnv
lnameEnv (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> BareSpecLHName)
-> (GhcSpec
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> GhcSpec
-> BareSpecLHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
_gsLSpec


-------------------------------------------------------------------------------------
-- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
--   validates it using @checkGhcSpec@.
-------------------------------------------------------------------------------------
makeGhcSpec :: [Ghc.Name]
            -> Config
            -> LogicNameEnv
            -> Bare.LocalVars
            -> GhcSrc
            -> LogicMap
            -> Ms.BareSpec
            -> [(ModName, Ms.BareSpec)]
            -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
-------------------------------------------------------------------------------------
makeGhcSpec :: [Name]
-> Config
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec [Name]
stratNames Config
cfg LogicNameEnv
lenv LocalVars
localVars GhcSrc
src LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs = do
  ghcTyLookupEnv <- [Bind Var] -> TcRn GHCTyLookupEnv
Bare.makeGHCTyLookupEnv (GhcSrc -> [Bind Var]
_giCbs GhcSrc
src)
  tcg <- Ghc.getGblEnv
  instEnvs <- Ghc.tcGetInstEnvs
  (dg0, sp) <- makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs
  let diagnostics = [Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> TargetSrc
-> SEnv SortedReft
-> [Bind Var]
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a. a -> [a] -> [a]
: ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a b. (a -> b) -> [a] -> [b]
map (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs)
                                         (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src)
                                         (GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp)
                                         (GhcSrc -> [Bind Var]
_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 b a. Hashable b => [(b, a)] -> SEnvB b 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}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, PPrint r, IsReft r,
 SubsTy
   RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)) r) =>
RRType r -> SortedReft
rSort SpecType
t) | (Symbol
x, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas     (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v, SpecType -> SortedReft
forall {r}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, PPrint r, IsReft r,
 SubsTy
   RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)) r) =>
RRType r -> SortedReft
rSort SpecType
t) | (Var
v, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(Var, Located SpecType)]
gsCtors    (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v, Var -> SortedReft
vSort Var
v) | Var
v               <- GhcSpecRefl -> [Var]
gsReflects (GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
sp)]
                 , [(Symbol
x, Sort -> ReftBV Symbol Symbol -> SortedReft
RR Sort
s ReftBV Symbol Symbol
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- [(Symbol, Sort)]
wiredSortedSyms       ]
                 , [(Symbol
x, Sort -> ReftBV Symbol Symbol -> SortedReft
RR Sort
s ReftBV Symbol Symbol
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp       ]
                 ]
    vSort :: Var -> SortedReft
vSort     = SpecType -> SortedReft
forall {r}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, PPrint r, IsReft r,
 SubsTy
   RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)) r) =>
RRType r -> SortedReft
rSort (SpecType -> SortedReft) -> (Var -> SpecType) -> Var -> 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) -> (Var -> SpecType) -> Var -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (Type -> SpecType
forall r. IsReft r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) (Type -> SpecType) -> (Var -> Type) -> Var -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
Ghc.varType
    rSort :: RRType r -> SortedReft
rSort     = TCEmb TyCon -> RRType r -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy
   RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)) 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
  :: [Ghc.Name]
  -> Config
  -> Bare.GHCTyLookupEnv
  -> Ghc.TcGblEnv
  -> Ghc.InstEnvs
  -> LogicNameEnv
  -> Bare.LocalVars
  -> GhcSrc
  -> LogicMap
  -> Ms.BareSpec
  -> [(ModName, Ms.BareSpec)]
  -> Ghc.TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 :: [Name]
-> Config
-> GHCTyLookupEnv
-> TcGblEnv
-> InstEnvs
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 [Name]
stratNames Config
cfg GHCTyLookupEnv
ghcTyLookupEnv TcGblEnv
tcg InstEnvs
instEnvs LogicNameEnv
lenv LocalVars
localVars GhcSrc
src LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs = do
  globalRdrEnv <- TcGblEnv -> OccEnv [GlobalRdrEltX GREInfo]
Ghc.tcg_rdr_env (TcGblEnv -> OccEnv [GlobalRdrEltX GREInfo])
-> TcRnIf TcGblEnv TcLclEnv TcGblEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (OccEnv [GlobalRdrEltX GREInfo])
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
  -- This spec is used to add lifted measures.
  let lSpec1   = Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1
  -- 'mySpec' and 'specs' contain the result of the first lifting stages, see [NOTE]: REFLECT-IMPORTS
  -- and the expanded aliases obtained using 'rtEnv'. 'myRTE' is a filtered 'rtEnv' used at the final
  -- lifting.
  let mySpec   = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec2 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Semigroup a => a -> a -> a
<> Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
lSpec1
  let specs    = ModName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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 stratNames 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 -> [(Var, Located SpecType, Equation)]
gsHAxioms GhcSpecRefl
refl
  let (dg4, measEnv) = withDiagnostics $ addOpaqueReflMeas cfg tycEnv env mySpec measEnv0 specs eqs
  let qual = Config
-> Env
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> GhcSpecQual
makeSpecQual Config
cfg Env
env OccEnv [GlobalRdrEltX GREInfo]
globalRdrEnv TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> GhcSpecData
makeSpecData  GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs
  let finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
lSpec0 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Semigroup a => a -> a -> a
<> Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
L.sort ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ (Var,
 Measure
   (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
   (Located LHName))
-> Var
forall a b. (a, b) -> a
fst ((Var,
  Measure
    (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    (Located LHName))
 -> Var)
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))]
-> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (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 ++ [bareSpec]
                , embeds = Ms.embeds bareSpec
                , privateReflects = mconcat $ map (privateReflects . snd) mspecs
                , defines = Ms.defines bareSpec
                , usedDataCons = usedDcs
                  -- Placing the @bareSpec@ at the end causes local aliases
                  -- to take precedence over imported ones when their names clash.
                  -- Alternatively, the last among @dependencySpecs@ (which is
                  -- ordered lexcographically) is picked.
                  -- See @tests/name/pos/ImportedTypeAlias.hs@
                , aliases = M.elems $ M.fromList $
                    [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt)
                    | rt <- concat $
                        map (aliases . snd) dependencySpecs ++
                        [expandedAliasesOf myRTE typeAliases $ aliases bareSpec]
                    ]
                , ealiases = M.elems $ M.fromList $
                    [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt)
                    | rt <- concat $
                        map (ealiases . snd) dependencySpecs ++
                        [expandedAliasesOf myRTE exprAliases $ ealiases mySpec1']
                    ]
                }
    })
  where
    thisModule :: GenModule Unit
thisModule = TcGblEnv -> GenModule Unit
Ghc.tcg_mod TcGblEnv
tcg
    expandedAliasesOf :: p -> (p -> HashMap LHName b) -> [RTAlias x a] -> [b]
expandedAliasesOf p
myRTE p -> HashMap LHName b
fld = (RTAlias x a -> Maybe b) -> [RTAlias x a] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((LHName -> HashMap LHName b -> Maybe b
forall k v. Hashable k => k -> HashMap k v -> Maybe v
`M.lookup` p -> HashMap LHName b
fld p
myRTE) (LHName -> Maybe b)
-> (RTAlias x a -> LHName) -> RTAlias x a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias x a -> Located LHName) -> RTAlias x a -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName)

    -- typeclass elaboration

    coreToLg :: CoreExpr -> ExprBV Symbol Symbol
coreToLg CoreExpr
ce =
      case TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM (ExprBV Symbol Symbol)
-> Either Error (ExprBV Symbol Symbol)
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 (ExprBV Symbol Symbol)
CoreToLogic.coreToLogic CoreExpr
ce) of
        Left Error
msg -> Maybe SrcSpan -> [Char] -> ExprBV Symbol Symbol
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 ExprBV Symbol Symbol
e -> ExprBV Symbol Symbol
e
    elaborateSig :: GhcSpecSig
-> [(Var, Located SpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
si [(Var, Located SpecType)]
auxsig = do
      tySigs <-
        [(Var, Located SpecType)]
-> ((Var, Located SpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (Var, Located SpecType))
-> TcRn [(Var, Located SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
si) (((Var, Located SpecType)
  -> IOEnv (Env TcGblEnv TcLclEnv) (Var, Located SpecType))
 -> TcRn [(Var, Located SpecType)])
-> ((Var, Located SpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (Var, Located SpecType))
-> TcRn [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ \(Var
x, Located SpecType
t) ->
          if Var -> Bool
forall a. NamedThing a => a -> Bool
GM.isFromGHCReal Var
x then
            (Var, Located SpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Var, Located SpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var
x, Located SpecType
t)
          else do t' <- (SpecType -> TcRn SpecType)
-> Located SpecType
-> IOEnv (Env TcGblEnv TcLclEnv) (Located SpecType)
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 -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> ExprBV Symbol Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) Located SpecType
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
    -- Specs with type and expression aliases expanded.
    mySpec2 :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec2  = BareRTEnv
-> SourcePos
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-mySpec2") Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1
    iSpecs2 :: HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
iSpecs2  = BareRTEnv
-> SourcePos
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-iSpecs2") ([(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs)
    -- Environment for alias lookup and expansion.
    rtEnv :: BareRTEnv
rtEnv    = LogicNameEnv
-> ModName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> BareRTEnv
Bare.makeRTEnv LogicNameEnv
lenv ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1' [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs
    mspecs :: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
mspecs   = (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec0) (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. a -> [a] -> [a]
: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs
    -- mySpec0 adds typeclass methods to the bare spec.
    (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec0, [(ClsInst, [Var])]
instMethods)  = if Bool
allowTC
                              then GhcSrc
-> Env
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> (Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
    [(ClsInst, [Var])])
Bare.compileClasses GhcSrc
src Env
env (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec) [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs
                              else (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec, [])
    mySpec1' :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1' = Env
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
addDefinesToExprAliases Env
env LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1
    -- Ready for alias expansion.
    mySpec1 :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec1  = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec0 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Semigroup a => a -> a -> a
<> Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
lSpec0
    -- This spec just has the 'ealiases' (with Haskell inlines) and 'dataDecls' fields.
    lSpec0 :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
lSpec0   = Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec0
    embs :: TCEmb TyCon
embs     = GhcSrc
-> GHCTyLookupEnv
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> TCEmb TyCon
makeEmbeds          GhcSrc
src GHCTyLookupEnv
ghcTyLookupEnv (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec0 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a. a -> [a] -> [a]
: ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a b. (a -> b) -> [a] -> [b]
map (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs)
    dm :: DataConMap
dm       = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv0
    (Diagnostics
dg0, [Located DataConP]
datacons, TycEnv
tycEnv0) = Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0   Config
cfg ModName
name Env
env TCEmb TyCon
embs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec2 HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
iSpecs2
    env :: Env
env      = Config
-> GHCTyLookupEnv
-> [Var]
-> TcGblEnv
-> InstEnvs
-> LocalVars
-> GhcSrc
-> LogicMap
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Env
Bare.makeEnv Config
cfg GHCTyLookupEnv
ghcTyLookupEnv [Var]
dataConIds TcGblEnv
tcg InstEnvs
instEnvs LocalVars
localVars GhcSrc
src LogicMap
lmap ((ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec) (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. a -> [a] -> [a]
: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> ModName
forall a b. (a, b) -> a
fst ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> ModName)
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
mspecs)

    usedDcs :: HashSet LHName
usedDcs  = [Bind Var]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> HashSet LHName
collectAllDataCons (GhcSrc -> [Bind Var]
_giCbs GhcSrc
src) ([Spec
    Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
 -> HashSet LHName)
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> HashSet LHName
forall a b. (a -> b) -> a -> b
$ Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bareSpec Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a. a -> [a] -> [a]
: ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a b. (a -> b) -> [a] -> [b]
map (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
dependencySpecs
    dataConIds :: [Var]
dataConIds =
      [ DataCon -> Var
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 :: [Bind Var]
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> HashSet LHName
collectAllDataCons [Bind Var]
cbs =
    [HashSet LHName] -> HashSet LHName
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet LHName] -> HashSet LHName)
-> ([Spec
       Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> [HashSet LHName])
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> [HashSet LHName])
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> [HashSet LHName])
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [HashSet LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> HashSet LHName)
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [HashSet LHName]
forall a b. (a -> b) -> [a] -> [b]
map Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> 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. 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
$
      [Bind Var] -> [Coercion]
collectCastCoercions [Bind Var]
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. 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
      | Var
v <- HashSet Var -> [Bind Var] -> [Var]
forall a. CBVisitable a => HashSet Var -> a -> [Var]
freeVars HashSet Var
forall a. HashSet a
S.empty [Bind Var]
cbs
      , DataCon
dc <- case HasCallStack => Var -> IdDetails
Var -> IdDetails
Ghc.idDetails Var
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 <- HasDebugCallStack => Coercion -> Pair Type
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 :: [Bind Var] -> [Coercion]
collectCastCoercions = [Coercion] -> [CoreExpr] -> [Coercion]
forall {b}. [Coercion] -> [Expr b] -> [Coercion]
gos [] ([CoreExpr] -> [Coercion])
-> ([Bind Var] -> [CoreExpr]) -> [Bind Var] -> [Coercion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bind Var -> [CoreExpr]) -> [Bind Var] -> [CoreExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Bind Var -> [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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Symbol, Sort)]
makeImports [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs = ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [(Symbol, Sort)])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Symbol, Sort)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Symbol, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> [(Symbol, Sort)])
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd) [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs'
  where specs' :: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs' = ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Bool)
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> Bool
isSrcImport (ModName -> Bool)
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> ModName)
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> ModName
forall a b. (a, b) -> a
fst) [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs


makeEmbeds :: GhcSrc -> Bare.GHCTyLookupEnv -> [Ms.BareSpec] -> F.TCEmb Ghc.TyCon
makeEmbeds :: GhcSrc
-> GHCTyLookupEnv
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> TCEmb TyCon
makeEmbeds GhcSrc
src GHCTyLookupEnv
env
  = TCEmb TyCon -> TCEmb TyCon
addBoolEmbed
  (TCEmb TyCon -> TCEmb TyCon)
-> ([Spec
       Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> TCEmb TyCon)
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> TCEmb TyCon)
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
    -> [TCEmb TyCon])
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> TCEmb TyCon)
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [TCEmb TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (GHCTyLookupEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TCEmb TyCon
makeTyConEmbeds GHCTyLookupEnv
env)

-- | Add the bool embedding
--
-- This is equivalent to the user adding the annotation
--
-- > {-@ embed Bool as bool @-}
--
-- It is needed by --adt, which produces checkers that
-- return a Bool. Without this embed annotation, the SMT solver would
-- reject the checkers as ill-sorted.
--
-- We used to have an embed annotation in LHAssumption modules, but it
-- was not in effect when the user did not import the necessary modules.
--
addBoolEmbed :: F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon
addBoolEmbed :: TCEmb TyCon -> TCEmb TyCon
addBoolEmbed TCEmb TyCon
embs
  | Maybe (Sort, TCArgs) -> Bool
forall a. Maybe a -> Bool
Mb.isJust (TyCon -> TCEmb TyCon -> Maybe (Sort, TCArgs)
forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
Ghc.boolTyCon TCEmb TyCon
embs) = TCEmb TyCon
embs
  | Bool
otherwise                                  = TyCon -> Sort -> TCArgs -> TCEmb TyCon -> TCEmb TyCon
forall a.
(Eq a, Hashable a) =>
a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsert TyCon
Ghc.boolTyCon Sort
F.boolSort TCArgs
F.NoArgs TCEmb TyCon
embs

makeTyConEmbeds :: Bare.GHCTyLookupEnv -> Ms.BareSpec -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: GHCTyLookupEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TCEmb TyCon
makeTyConEmbeds GHCTyLookupEnv
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> TCEmb (Located LHName)
forall lname ty. Spec lname ty -> TCEmb (Located LHName)
Ms.embeds Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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

-- | See [NOTE:EXPRESSION-ALIASES]
addDefinesToExprAliases :: Bare.Env -> LogicMap -> Ms.BareSpec -> Ms.BareSpec
addDefinesToExprAliases :: Env
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
addDefinesToExprAliases Env
env LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec =
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec {
    Ms.ealiases = Ms.ealiases mySpec ++
      if typeclass (getConfig env) then []
      -- lmap expansion happens during elaboration
      -- this clearly breaks things if a signature
      -- contains lmap functions but never gets
      -- elaborated
      else [ e | (_, xl) <- M.toList (lmSymDefs lmap), let e = LMapV Symbol -> RTAlias Symbol (ExprBV Symbol Symbol)
lmapEAlias LMapV Symbol
xl ]
    }

--------------------------------------------------------------------------------
-- | [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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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. Here is relevant to
-- [NOTE:EXPRESSION-ALIASES].
--------------------------------------------------------------------------------
makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                -> Ms.BareSpec
makeLiftedSpec0 :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Monoid a => a
mempty
  { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines cfg src embs lmap mySpec
  , Ms.dataDecls = Bare.makeHaskellDataDecls 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       = TCEmb TyCon
-> [Bind Var]
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [TyCon]
reflectedTyCons TCEmb TyCon
embs [Bind Var]
cbs  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec
    cbs :: [Bind Var]
cbs          = GhcSrc -> [Bind Var]
_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. 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.
--
--   We collect TyCons from the data constructors actually used in the bodies of
--   reflected functions and measure functions, rather than those mentioned in
--   their type signatures. This avoids generating selectors for types that are
--   only referenced in signatures but not actually pattern-matched.

reflectedTyCons :: TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]
reflectedTyCons :: TCEmb TyCon
-> [Bind Var]
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [TyCon]
reflectedTyCons TCEmb TyCon
embs [Bind Var]
cbs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec =
    [ TyCon
tyCon
    | Var
fv <- HashSet Var -> [Bind Var] -> [Var]
forall a. CBVisitable a => HashSet Var -> a -> [Var]
freeVars HashSet Var
forall a. HashSet a
S.empty [Bind Var]
relevantBinds
    , DataCon
dc <- case HasCallStack => Var -> IdDetails
Var -> IdDetails
Ghc.idDetails Var
fv of
        Ghc.DataConWrapId DataCon
dc -> [DataCon
dc]
        Ghc.DataConWorkId DataCon
dc -> [DataCon
dc]
        IdDetails
_                    -> []
    , let tyCon :: TyCon
tyCon = DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc
    , Bool -> Bool
not (TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs TyCon
tyCon)
    ]
  where
    reflMeasVarSet :: HashSet Var
reflMeasVarSet = [Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Var] -> HashSet Var) -> [Var] -> HashSet Var
forall a b. (a -> b) -> a -> b
$ Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Bind Var] -> [Var]
reflectedVars Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec [Bind Var]
cbs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Bind Var] -> [Var]
measureVars Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec [Bind Var]
cbs
    relevantBinds :: [Bind Var]
relevantBinds  = (Bind Var -> Bool) -> [Bind Var] -> [Bind Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (HashSet Var -> Bind Var -> Bool
isRelevantBind HashSet Var
reflMeasVarSet) [Bind Var]
cbs

isRelevantBind :: S.HashSet Ghc.Var -> Ghc.CoreBind -> Bool
isRelevantBind :: HashSet Var -> Bind Var -> Bool
isRelevantBind HashSet Var
vars (Ghc.NonRec Var
v CoreExpr
_) = Var
v Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet Var
vars
isRelevantBind HashSet Var
vars (Ghc.Rec [(Var, CoreExpr)]
pairs)  = ((Var, CoreExpr) -> Bool) -> [(Var, CoreExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet Var
vars) (Var -> Bool)
-> ((Var, CoreExpr) -> Var) -> (Var, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst) [(Var, CoreExpr)]
pairs

-- | 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

reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
reflectedVars :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Bind Var] -> [Var]
reflectedVars Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec [Bind Var]
cbs =
    (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (Located LHName -> Bool
isReflSym (Located LHName -> Bool) -> (Var -> Located LHName) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Located LHName
makeGHCLHNameLocatedFromId)
      ([Bind Var] -> [Var]
forall b. [Bind b] -> [b]
Ghc.bindersOfBinds [Bind Var]
cbs)
  where
    isReflSym :: Located LHName -> Bool
isReflSym Located LHName
x =
      Located LHName -> HashSet (Located LHName) -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Located LHName
x (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) Bool -> Bool -> Bool
||
      Located Symbol -> HashSet (Located Symbol) -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member ((LHName -> Symbol) -> Located LHName -> Located Symbol
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located Symbol)
forall lname ty. Spec lname ty -> HashSet (Located Symbol)
Ms.privateReflects Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec)

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

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
             -> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars :: Config
-> GhcSrc
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec Env
env MeasEnv
measEnv = do
  let tgtVars :: [Var]
tgtVars = ([Char] -> Maybe Var) -> [[Char]] -> [Var]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ([Char] -> HashMap [Char] Var -> Maybe Var
forall k v. Hashable k => k -> HashMap k v -> Maybe v
`M.lookup` HashMap [Char] Var
hvars) (Config -> [[Char]]
checks     Config
cfg)
  igVars      <-  (Located LHName -> Either [Error] Var)
-> HashSet (Located LHName) -> Either [Error] (HashSet Var)
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] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env) (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.ignores Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec)
  lVars       <-  sMapM (Bare.lookupGhcIdLHName env) (Ms.lvars   mySpec)
  return (SpVar tgtVars igVars lVars cMethods)
  where
    cMethods :: [Var]
cMethods   = (ModName, Var, Located SpecType) -> Var
forall a b c. (a, b, c) -> b
snd3 ((ModName, Var, Located SpecType) -> Var)
-> [(ModName, Var, Located SpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(ModName, Var, Located SpecType)]
Bare.meMethods MeasEnv
measEnv
    hvars :: HashMap [Char] Var
hvars = [([Char], Var)] -> HashMap [Char] Var
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList
      [ (OccName -> [Char]
Ghc.occNameString (OccName -> [Char]) -> OccName -> [Char]
forall a b. (a -> b) -> a -> b
$ Var -> OccName
forall a. NamedThing a => a -> OccName
Ghc.getOccName Var
b, Var
b)
      | Var
b <- [Bind Var] -> [Var]
forall b. [Bind b] -> [b]
Ghc.bindersOfBinds (GhcSrc -> [Bind Var]
_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
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> GhcSpecQual
makeSpecQual Config
_cfg Env
env OccEnv [GlobalRdrEltX GREInfo]
globalRdrEnv TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
_rtEnv Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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}. (Variable a ~ Symbol, 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
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [QualifierV Symbol]
forall ty.
Env
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> Spec Symbol ty
-> [QualifierV Symbol]
makeQualifiers Env
env OccEnv [GlobalRdrEltX GREInfo]
globalRdrEnv TycEnv
tycEnv Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++
      (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> [QualifierV Symbol])
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [QualifierV Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [QualifierV Symbol]
forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers (HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall k v. HashMap k v -> [v]
M.elems HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet Symbol
mSyms) (a -> [Variable a]
forall a. Subable a => a -> [Variable a]
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. 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 (ReftBV Symbol Symbol))) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType (ReftBV Symbol Symbol))) -> Symbol)
-> [(Symbol, Located (RRType (ReftBV Symbol Symbol)))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType (ReftBV Symbol Symbol)))]
Bare.meSyms MeasEnv
measEnv)
                   [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Located (RRType (ReftBV Symbol Symbol))) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType (ReftBV Symbol Symbol))) -> Symbol)
-> [(Symbol, Located (RRType (ReftBV Symbol Symbol)))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType (ReftBV Symbol Symbol)))]
Bare.meClassSyms MeasEnv
measEnv)

makeQualifiers
  :: Bare.Env
  -> Ghc.GlobalRdrEnv
  -> Bare.TycEnv
  -> Ms.Spec F.Symbol ty
  -> [F.Qualifier]
makeQualifiers :: forall ty.
Env
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> Spec Symbol ty
-> [QualifierV Symbol]
makeQualifiers Env
env OccEnv [GlobalRdrEltX GREInfo]
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
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> QualifierV Symbol
-> Maybe (QualifierV Symbol)
resolveQParams Env
env OccEnv [GlobalRdrEltX GREInfo]
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
-> OccEnv [GlobalRdrEltX GREInfo]
-> TycEnv
-> QualifierV Symbol
-> Maybe (QualifierV Symbol)
resolveQParams Env
env OccEnv [GlobalRdrEltX GREInfo]
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
-> OccEnv [GlobalRdrEltX GREInfo] -> TycEnv -> FTycon -> Maybe Sort
qualifyFTycon Env
env OccEnv [GlobalRdrEltX GREInfo]
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
-> OccEnv [GlobalRdrEltX GREInfo] -> TycEnv -> FTycon -> Maybe Sort
qualifyFTycon Env
env OccEnv [GlobalRdrEltX GREInfo]
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
. Located Symbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Symbol
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 OccEnv [GlobalRdrEltX GREInfo]
-> Located Symbol -> Either Error (Located LHName)
resolveSymbolToTcName OccEnv [GlobalRdrEltX GREInfo]
globalRdrEnv Located Symbol
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           = Located Symbol -> Symbol
forall a. Located a -> a
F.val Located Symbol
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 :: Located Symbol
tcs                 = FTycon -> Located Symbol
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
. Located Symbol -> FTycon
F.symbolFTycon (Located Symbol -> FTycon)
-> (Located TyCon -> Located Symbol) -> Located TyCon -> FTycon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Symbol) -> Located TyCon -> Located Symbol
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> LogicNameEnv
-> Env
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec LogicNameEnv
lenv Env
env = do
  sizes  <- if Config -> Bool
forall a. HasConfig a => a -> Bool
structuralTerm Config
cfg then HashSet Var -> Either [Error] (HashSet Var)
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet Var
forall a. Monoid a => a
mempty else LogicNameEnv
-> Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
makeSize LogicNameEnv
lenv Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     RelExpr, RelExpr)]
-> Lookup
     [(Var, Var, Located SpecType, Located SpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv = ((Located LHName, Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
  RelExpr, RelExpr)
 -> Either
      [Error]
      (Var, Var, Located SpecType, Located SpecType, RelExpr, RelExpr))
-> [(Located LHName, Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     RelExpr, RelExpr)]
-> Lookup
     [(Var, Var, Located SpecType, Located SpecType, 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 RelExpr, RelExpr)
-> Either
     [Error]
     (Var, Var, Located SpecType, Located SpecType, RelExpr, RelExpr)
forall {e} {f}.
(Located LHName, Located LHName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)), e,
 f)
-> Either
     [Error] (Var, Var, Located SpecType, Located SpecType, e, f)
go
 where
  go :: (Located LHName, Located LHName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)), e,
 f)
-> Either
     [Error] (Var, Var, Located SpecType, Located SpecType, e, f)
go (Located LHName
x, Located LHName
y, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
tx, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
ty, e
a, f
e) = do
    vx <- HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
makeLazy Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec =
  (Located LHName -> Either [Error] Var)
-> HashSet (Located LHName) -> Either [Error] (HashSet Var)
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] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env) (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.lazy Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec)

makeFail :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail :: Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup (HashSet (Located Var))
makeFail Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec =
  HashSet (Located LHName)
-> (Located LHName -> Either [Error] (Located Var))
-> Lookup (HashSet (Located Var))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.fails Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) ((Located LHName -> Either [Error] (Located Var))
 -> Lookup (HashSet (Located Var)))
-> (Located LHName -> Either [Error] (Located Var))
-> Lookup (HashSet (Located Var))
forall a b. (a -> b) -> a -> b
$ \Located LHName
x -> do
    vx <- HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup (HashSet (Located Var))
makeRewrite Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec =
  HashSet (Located LHName)
-> (Located LHName -> Either [Error] (Located Var))
-> Lookup (HashSet (Located Var))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.rewrites Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) ((Located LHName -> Either [Error] (Located Var))
 -> Lookup (HashSet (Located Var)))
-> (Located LHName -> Either [Error] (Located Var))
-> Lookup (HashSet (Located Var))
forall a b. (a -> b) -> a -> b
$ \Located LHName
x -> do
    vx <-  HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup (HashMap Var [Var])
makeRewriteWith Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec = [(Var, [Var])] -> HashMap Var [Var]
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(Var, [Var])] -> HashMap Var [Var])
-> Either [Error] [(Var, [Var])] -> Lookup (HashMap Var [Var])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] [(Var, [Var])]
forall lname ty.
Env -> Spec lname ty -> Either [Error] [(Var, [Var])]
makeRewriteWith' Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec

makeRewriteWith' :: Bare.Env -> Spec lname ty -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall lname ty.
Env -> Spec lname ty -> Either [Error] [(Var, [Var])]
makeRewriteWith' Env
env Spec lname ty
spec =
  [(Located LHName, [Located LHName])]
-> ((Located LHName, [Located LHName])
    -> Either [Error] (Var, [Var]))
-> Either [Error] [(Var, [Var])]
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] (Var, [Var]))
 -> Either [Error] [(Var, [Var])])
-> ((Located LHName, [Located LHName])
    -> Either [Error] (Var, [Var]))
-> Either [Error] [(Var, [Var])]
forall a b. (a -> b) -> a -> b
$ \(Located LHName
x, [Located LHName]
xs) -> do
    xv  <- HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> 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. Hashable a => [a] -> HashSet a
S.fromList
  (Either [Error] [TyCon] -> Lookup (HashSet TyCon))
-> (Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> Either [Error] [TyCon])
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> [Located LHName])
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> HashSet (Located LHName))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
makeSize LogicNameEnv
lenv Env
env
  = ([Var] -> HashSet Var)
-> Either [Error] [Var] -> Either [Error] (HashSet Var)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList
  (Either [Error] [Var] -> Either [Error] (HashSet Var))
-> (Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> Either [Error] [Var])
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located Symbol -> Either [Error] Var)
-> [Located Symbol] -> Either [Error] [Var]
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 Symbol -> Either [Error] Var
lookupGhcSize
  ([Located Symbol] -> Either [Error] [Var])
-> (Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> [Located Symbol])
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Maybe (Located Symbol))
-> [DataDecl] -> [Located Symbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe (Located Symbol)
getSizeFuns
  ([DataDecl] -> [Located Symbol])
-> (Spec
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> [DataDecl])
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Located Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.dataDecls
  where
    lookupGhcSize :: LocSymbol -> Bare.Lookup Ghc.Var
    lookupGhcSize :: Located Symbol -> Either [Error] Var
lookupGhcSize Located Symbol
s =
      case Symbol -> SEnvB Symbol LHName -> Maybe LHName
forall b a. Hashable b => b -> SEnvB b a -> Maybe a
lookupSEnv (Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
s) (LogicNameEnv -> SEnvB Symbol LHName
lneLHName LogicNameEnv
lenv) of
        Maybe LHName
Nothing -> Maybe SrcSpan -> [Char] -> Either [Error] Var
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 Symbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located Symbol
s) ([Char] -> Either [Error] Var) -> [Char] -> Either [Error] Var
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 (Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
s)
        Just LHName
n -> case LHName -> Maybe Name
maybeReflectedLHName LHName
n of
          Maybe Name
Nothing -> Maybe SrcSpan -> [Char] -> Either [Error] Var
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 Symbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located Symbol
s) ([Char] -> Either [Error] Var) -> [Char] -> Either [Error] Var
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 (Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
s)
          Just Name
rn -> HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env (Name -> Symbol -> LHName
makeGHCLHName Name
rn (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
rn) LHName -> Located Symbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located Symbol
s)

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


------------------------------------------------------------------------------------------
makeSpecRefl :: GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
             -> Bare.Lookup GhcSpecRefl
------------------------------------------------------------------------------------------
makeSpecRefl :: GhcSrc
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl GhcSrc
src HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
  autoInst <- Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
makeAutoInst Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 = (Var, Located SpecType, Equation) -> Equation
forall a b c. (a, b, c) -> c
thd3 ((Var, Located SpecType, Equation) -> Equation)
-> [(Var, Located SpecType, Equation)] -> [Equation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Located SpecType, Equation)]
asmReflAxioms
  let myAxioms =
        [ Equation
e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
        | (Var
_, Located SpecType
_, Equation
e) <- [(Var, Located SpecType, 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [Equation])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> [Equation])
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Equation]
forall lname ty. Spec lname ty -> [EquationV lname]
Ms.axeqs (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> [Equation])
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd) (HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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 Var
gsAutoInst   = HashSet Var
autoInst
      , gsImpAxioms :: [Equation]
gsImpAxioms  = [Equation]
impAxioms
      , gsMyAxioms :: [Equation]
gsMyAxioms   = [Equation]
myAxioms
      , gsReflects :: [Var]
gsReflects   = ((Var, Located SpecType, Equation) -> Var
forall a b c. (a, b, c) -> a
fst3 ((Var, Located SpecType, Equation) -> Var)
-> [(Var, Located SpecType, Equation)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Located SpecType, Equation)]
xtes) [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ ((Var, Var) -> Var
forall a b. (a, b) -> a
fst ((Var, Var) -> Var) -> [(Var, Var)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(Var, Var)]
gsAsmReflects GhcSpecSig
sig)
      , gsHAxioms :: [(Var, Located SpecType, Equation)]
gsHAxioms    = [Char]
-> [(Var, Located SpecType, Equation)]
-> [(Var, Located SpecType, Equation)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsHAxioms" ([(Var, Located SpecType, Equation)]
 -> [(Var, Located SpecType, Equation)])
-> [(Var, Located SpecType, Equation)]
-> [(Var, Located SpecType, Equation)]
forall a b. (a -> b) -> a -> b
$ [(Var, Located SpecType, Equation)]
xtes [(Var, Located SpecType, Equation)]
-> [(Var, Located SpecType, Equation)]
-> [(Var, Located SpecType, Equation)]
forall a. [a] -> [a] -> [a]
++ [(Var, Located SpecType, Equation)]
asmReflAxioms
      , gsRewrites :: HashSet (Located Var)
gsRewrites   = HashSet (Located Var)
rwr
      , gsRewritesWith :: HashMap Var [Var]
gsRewritesWith = HashMap Var [Var]
rwrWith
      }
  where
    mySpec :: Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec       = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> ModName
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Monoid a => a
mempty ModName
name HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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. Hashable a => a -> HashSet a -> Bool
`S.member` Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec Bool -> Bool -> Bool
||
      (LHName -> Symbol) -> Located LHName -> Located Symbol
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 Located Symbol -> HashSet (Located Symbol) -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located Symbol)
forall lname ty. Spec lname ty -> HashSet (Located Symbol)
Ms.privateReflects Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 :: [(Var, Located SpecType)]
combinedOpaqueAndReflectedAsmSigs = HashMap Var (Located SpecType) -> [(Var, Located SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var (Located SpecType) -> [(Var, Located SpecType)])
-> HashMap Var (Located SpecType) -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$
        [(Var, Located SpecType)] -> HashMap Var (Located SpecType)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList (Var -> (Var, Located SpecType)
createUpdatedSpecs (Var -> (Var, Located SpecType))
-> ((Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))
    -> Var)
-> (Var,
    Measure
      (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
      (Located LHName))
-> (Var, Located SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var,
 Measure
   (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
   (Located LHName))
-> Var
forall a b. (a, b) -> a
fst ((Var,
  Measure
    (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    (Located LHName))
 -> (Var, Located SpecType))
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))]
-> [(Var, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))]
Bare.meOpaqueRefl MeasEnv
measEnv)
        HashMap Var (Located SpecType)
-> HashMap Var (Located SpecType) -> HashMap Var (Located SpecType)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
`M.union` [(Var, Located SpecType)] -> HashMap Var (Located SpecType)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList (((Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var, Located SpecType) -> Bool
forall {b}. (Var, b) -> Bool
notReflected (GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs GhcSpecSig
sig))
    -- Strengthen the post-condition of each of the opaque reflections.
    createUpdatedSpecs :: Var -> (Var, Located SpecType)
createUpdatedSpecs Var
var = (Var
var, AxiomType -> SpecType
Bare.aty (AxiomType -> SpecType) -> Located AxiomType -> Located SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> Env -> Var -> Located Symbol -> Located AxiomType
Bare.strengthenSpecWithMeasure GhcSpecSig
sig Env
env Var
var (Var -> Located Symbol
Bare.varLocSym Var
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 :: (Var, Located SpecType) -> (Var, Located SpecType)
expandReflectedSignature = (Located SpecType -> Located SpecType)
-> (Var, Located SpecType) -> (Var, Located SpecType)
forall a b. (a -> b) -> (Var, a) -> (Var, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> SourcePos -> Located SpecType -> Located SpecType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-refSigs"))

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

makeAutoInst :: Bare.Env -> Ms.BareSpec ->
                Bare.Lookup (S.HashSet Ghc.Var)
makeAutoInst :: Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (HashSet Var)
makeAutoInst Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec = [Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Var] -> HashSet Var)
-> Either [Error] [Var] -> Either [Error] (HashSet Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [Var]
kvs
  where
    kvs :: Either [Error] [Var]
kvs = [Located LHName]
-> (Located LHName -> Either [Error] Var) -> Either [Error] [Var]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.autois Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec)) ((Located LHName -> Either [Error] Var) -> Either [Error] [Var])
-> (Located LHName -> Either [Error] Var) -> Either [Error] [Var]
forall a b. (a -> b) -> a -> b
$
            HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env


----------------------------------------------------------------------------------------
makeSpecSig :: [Ghc.Name] -> Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
            -> Bare.Lookup ([RInstance LocBareType], GhcSpecSig)
----------------------------------------------------------------------------------------
makeSpecSig :: [Name]
-> Config
-> ModName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [Bind Var]
-> Lookup
     ([RInstance
         (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))],
      GhcSpecSig)
makeSpecSig [Name]
stratNames Config
cfg ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [Bind Var]
cbs = do
  mySigs     <- Env
-> SigEnv
-> ModName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup
     [(Var, Located SpecType, Maybe [Located (ExprBV Symbol Symbol)])]
makeTySigs  Env
env SigEnv
sigEnv ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec
  aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs
  let asmSigs =  TycEnv -> [(Var, Located SpecType)]
Bare.tcSelVars TycEnv
tycEnv [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ [(Var, Located SpecType)]
aSigs
  let tySigs  = [(Var, (Int, Located SpecType))] -> [(Var, Located SpecType)]
strengthenSigs ([(Var, (Int, Located SpecType))] -> [(Var, Located SpecType)])
-> ([[(Var, (Int, Located SpecType))]]
    -> [(Var, (Int, Located SpecType))])
-> [[(Var, (Int, Located SpecType))]]
-> [(Var, Located SpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Var, (Int, Located SpecType))]]
-> [(Var, (Int, Located SpecType))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Var, (Int, Located SpecType))]] -> [(Var, Located SpecType)])
-> [[(Var, (Int, Located SpecType))]] -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$
                  [ [(Var
v, (Int
0, Located SpecType
t)) | (Var
v, Located SpecType
t,Maybe [Located (ExprBV Symbol Symbol)]
_) <- [(Var, Located SpecType, Maybe [Located (ExprBV Symbol Symbol)])]
mySigs                         ]   -- NOTE: these weights are to priortize
                  , [(Var
v, (Int
1, Located SpecType
t)) | (Var
v, Located SpecType
t  ) <- MeasEnv -> [(Var, Located SpecType)]
makeMthSigs MeasEnv
measEnv            ]   -- user defined sigs OVER auto-generated
                  , [(Var
v, (Int
2, Located SpecType
t)) | (Var
v, Located SpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
allSpecs ]   -- during the strengthening, i.e. to KEEP
                  , [(Var
v, (Int
3, Located SpecType
t)) | (Var
v, Located SpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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
    , gsStratCtos = stratNames
    , 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
instances, DEnv Var (Located SpecType)
dicts) = Env
-> SigEnv
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> ([RInstance
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))],
    DEnv Var (Located SpecType))
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec) (HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs)
    allSpecs :: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
allSpecs   = (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec) (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. a -> [a] -> [a]
: HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs
    rtEnv :: BareRTEnv
rtEnv      = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    getVar :: Located LHName -> Var
getVar Located LHName
sym = case HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env Located LHName
sym of
      Right Var
x -> Var
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> Var
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 :: [(Var, (Int, Located SpecType))] -> [(Var, Located SpecType)]
strengthenSigs [(Var, (Int, Located SpecType))]
sigs = (Var, [(Int, Located SpecType)]) -> (Var, Located SpecType)
forall {a} {b}.
(PPrint a, Ord b) =>
(a, [(b, Located SpecType)]) -> (a, Located SpecType)
go ((Var, [(Int, Located SpecType)]) -> (Var, Located SpecType))
-> [(Var, [(Int, Located SpecType)])] -> [(Var, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, (Int, Located SpecType))]
-> [(Var, [(Int, Located SpecType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Var, (Int, Located SpecType))]
sigs
  where
    go :: (a, [(b, Located SpecType)]) -> (a, Located SpecType)
go (a
v, [(b, Located SpecType)]
ixs)     = (a
v,) (Located SpecType -> (a, Located SpecType))
-> Located SpecType -> (a, Located SpecType)
forall a b. (a -> b) -> a -> b
$ (Located SpecType -> Located SpecType -> Located SpecType)
-> [Located SpecType] -> Located SpecType
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
L.foldl1' ((Located SpecType -> Located SpecType -> Located SpecType)
-> Located SpecType -> Located SpecType -> Located SpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip Located SpecType -> Located SpecType -> Located SpecType
meetLoc) ([Char] -> [Located SpecType] -> [Located SpecType]
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, Located SpecType)] -> [Located SpecType]
forall {b} {b}. Ord b => [(b, b)] -> [b]
prio [(b, Located SpecType)]
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 :: Located SpecType -> Located SpecType -> Located SpecType
meetLoc Located SpecType
t1 Located SpecType
t2   = Located SpecType
t1 {val = val t1 `meet` val t2}

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

makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeInlSigs :: Env
-> BareRTEnv
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (Var -> SpecType) -> [Var] -> [(Var, Located SpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> Var -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([Var] -> [(Var, Located SpecType)])
-> ([(ModName,
      Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
    -> [Var])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [Var])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Located LHName -> Var) -> [Located LHName] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Located LHName -> Var
lookupFunctionId Env
env) ([Located LHName] -> [Var])
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> [Located LHName])
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Var]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> HashSet (Located LHName))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.inlines (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> HashSet (Located LHName))
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> HashSet (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd)

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs :: Env
-> BareRTEnv
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (Var -> SpecType) -> [Var] -> [(Var, Located SpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> Var -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([Var] -> [(Var, Located SpecType)])
-> ([(ModName,
      Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
    -> [Var])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var, Located SpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [Var])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Located LHName -> Var) -> [Located LHName] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Located LHName -> Var
lookupFunctionId Env
env) ([Located LHName] -> [Var])
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> [Located LHName])
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Var]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> HashSet (Located LHName))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> HashSet (Located LHName))
-> ((ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Spec
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> HashSet (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a, b) -> b
snd)

lookupFunctionId :: Bare.Env -> Located LHName -> Ghc.Id
lookupFunctionId :: Env -> Located LHName -> Var
lookupFunctionId Env
env Located LHName
x =
    ([Error] -> Var) -> (Var -> Var) -> Either [Error] Var -> Var
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe SrcSpan -> [Char] -> [Error] -> Var
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") Var -> Var
forall a. a -> a
id (Either [Error] Var -> Var) -> Either [Error] Var -> Var
forall a b. (a -> b) -> a -> b
$
    HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env Located LHName
x

makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
makeLiftedSigs :: BareRTEnv
-> (Var -> SpecType) -> [Var] -> [(Var, Located SpecType)]
makeLiftedSigs BareRTEnv
rtEnv Var -> SpecType
f [Var]
xs
  = [(Var
x, Located SpecType
lt) | Var
x <- [Var]
xs
             , let lx :: Located Var
lx = Var -> Located Var
forall a. NamedThing a => a -> Located a
GM.locNamedThing Var
x
             , let lt :: Located SpecType
lt = Located SpecType -> Located SpecType
expand (Located SpecType -> Located SpecType)
-> Located SpecType -> Located SpecType
forall a b. (a -> b) -> a -> b
$ Located Var
lx {val = f x}
    ]
  where
    expand :: Located SpecType -> Located SpecType
expand   = BareRTEnv -> Located SpecType -> Located SpecType
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup
     [(Var, Located SpecType, Maybe [Located (ExprBV Symbol Symbol)])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec = do
  bareSigs   <- Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
bareTySigs Env
env                     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
  expSigs    <- makeTExpr  env bareSigs rtEnv spec
  let rawSigs = Env
-> [(Var,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Maybe [Located (ExprBV Symbol Symbol)])]
-> [(Var,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Maybe [Located (ExprBV Symbol Symbol)])]
Bare.resolveLocalBinds Env
env [(Var,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
  Maybe [Located (ExprBV Symbol Symbol)])]
expSigs
  return [ (x, cook x bt, z) | (x, bt, z) <- rawSigs ]
  where
    rtEnv :: BareRTEnv
rtEnv     = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    cook :: Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
cook Var
x Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (Var -> PlugTV Var
forall v. v -> PlugTV v
Bare.HsTV Var
x) Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt

bareTySigs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs :: Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
bareTySigs Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec = [(Var,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Var,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs ([(Var,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
 -> [(Var,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lookup
  [(Var,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
vts
  where
    vts :: Lookup
  [(Var,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
vts = [(Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> ((Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Either
         [Error]
         (Var,
          Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
Ms.sigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec ) (((Located LHName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
  -> Either
       [Error]
       (Var,
        Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
 -> Lookup
      [(Var,
        Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])
-> ((Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Either
         [Error]
         (Var,
          Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
-> Lookup
     [(Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a b. (a -> b) -> a -> b
$ \ (Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) -> do
            v <- [Char] -> Either [Error] Var -> Either [Error] Var
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LOOKUP-GHC-VAR" (Either [Error] Var -> Either [Error] Var)
-> Either [Error] Var -> Either [Error] Var
forall a b. (a -> b) -> a -> b
$ HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup [(Var, Located SpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs = do
  raSigs <- Env
-> ModName
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup
     [(ModName, Var,
       Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
rawAsmSigs Env
env ModName
myName [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs
  return [ (x, t) | (name, x, bt) <- raSigs, let t = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (Var -> PlugTV Var
forall v. v -> PlugTV v
Bare.LqTV Var
x) Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt ]

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

myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: Var
-> [(Bool, ModName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> (ModName,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
myAsmSig Var
v [(Bool, ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
sigs = (ModName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Maybe
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (ModName,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall a. a -> Maybe a -> a
Mb.fromMaybe (ModName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall {a}. a
errImp (Maybe
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
mbHome Maybe
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Maybe
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Maybe
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
mbImp)
  where
    mbHome :: Maybe
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
mbHome      = ([(ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
 -> UserError)
-> [(ModName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Maybe
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr                  [(ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
mbImp       = ((ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> ModName)
-> [(ModName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Maybe
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall b a. Ord b => (a -> b) -> [a] -> Maybe a
takeBiggest   (ModName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> ModName
forall a b. (a, b) -> a
fst ([(Int,
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
-> [(ModName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int,
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
sigsImp) -- see [NOTE:Prioritize-Home-Spec]
    sigsHome :: [(ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
sigsHome    = [(ModName
m, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t)      | (Bool
True,  ModName
m, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) <- [(Bool, ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
sigs ]
    sigsImp :: [(Int,
  (ModName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
sigsImp     = [Char]
-> [(Int,
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
-> [(Int,
     (ModName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Var
v)
                  [(Int
d, (ModName
m, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t)) | (Bool
False, ModName
m, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) <- [(Bool, ModName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
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 (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan Var
v) (Var -> Doc
forall a. PPrint a => a -> Doc
F.pprint Var
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v)

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

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

makeVarTExprs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] [(Var, [Located (ExprBV Symbol Symbol)])]
makeVarTExprs Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec =
  [(Located LHName, [Located (ExprBV Symbol Symbol)])]
-> ((Located LHName, [Located (ExprBV Symbol Symbol)])
    -> Either [Error] (Var, [Located (ExprBV Symbol Symbol)]))
-> Either [Error] [(Var, [Located (ExprBV Symbol Symbol)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName, [Located (ExprBV Symbol Symbol)])]
forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
Ms.termexprs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) (((Located LHName, [Located (ExprBV Symbol Symbol)])
  -> Either [Error] (Var, [Located (ExprBV Symbol Symbol)]))
 -> Either [Error] [(Var, [Located (ExprBV Symbol Symbol)])])
-> ((Located LHName, [Located (ExprBV Symbol Symbol)])
    -> Either [Error] (Var, [Located (ExprBV Symbol Symbol)]))
-> Either [Error] [(Var, [Located (ExprBV Symbol Symbol)])]
forall a b. (a -> b) -> a -> b
$ \(Located LHName
x, [Located (ExprBV Symbol Symbol)]
es) -> do
    vx <- HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup
     [(Var,
       [(Bool, ModName,
         Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])]
allAsmSigs Env
env ModName
myName [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs = do
  let aSigs :: [(ModName, Bool, Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
aSigs = [ (ModName
name, Bool
locallyDefined, Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) | (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) <- [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs
                                   , (Bool
locallyDefined, Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) <- ModName
-> ModName
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Bool, Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
getAsmSigs ModName
myName ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec ]
  vSigs    <- [(ModName, Bool, Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> ((ModName, Bool, Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Either
         [Error]
         (Var,
          (Bool, ModName,
           Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))))
-> Either
     [Error]
     [(Var,
       (Bool, ModName,
        Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
aSigs (((ModName, Bool, Located LHName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
  -> Either
       [Error]
       (Var,
        (Bool, ModName,
         Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))))
 -> Either
      [Error]
      [(Var,
        (Bool, ModName,
         Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))])
-> ((ModName, Bool, Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Either
         [Error]
         (Var,
          (Bool, ModName,
           Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))))
-> Either
     [Error]
     [(Var,
       (Bool, ModName,
        Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))]
forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) -> do
                v <- HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 :: Var -> Bool
isUsedExternalVar Var
v = case HasCallStack => Var -> IdDetails
Var -> IdDetails
Ghc.idDetails Var
v of
      Ghc.DataConWrapId DataCon
dc ->
        Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName Var
v Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env
         Bool -> Bool -> Bool
||
        Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName (DataCon -> Var
Ghc.dataConWorkId DataCon
dc) Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env
      IdDetails
_ ->
        Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName Var
v Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env

    isInScope :: Ghc.Var -> Bool
    isInScope :: Var -> Bool
isInScope Var
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
$
            OccEnv [GlobalRdrEltX GREInfo]
-> Name -> Maybe (GlobalRdrEltX GREInfo)
forall info.
Outputable info =>
GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info)
Ghc.lookupGRE_Name
              (TcGblEnv -> OccEnv [GlobalRdrEltX GREInfo]
Ghc.tcg_rdr_env (TcGblEnv -> OccEnv [GlobalRdrEltX GREInfo])
-> TcGblEnv -> OccEnv [GlobalRdrEltX GREInfo]
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 HasCallStack => Var -> IdDetails
Var -> IdDetails
Ghc.idDetails Var
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
_ -> Var -> Bool
forall a. NamedThing a => a -> Bool
inScope Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Bool, Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
getAsmSigs ModName
myName ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
  | ModName
myName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True, Located LHName
x,  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) | (Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) <- Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
Ms.asmSigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec ] -- MUST    resolve, or error
  | Bool
otherwise      =
      [ (Bool
False, Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t)
      | (Located LHName
x, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t) <- Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
Ms.asmSigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
                  [(Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. [a] -> [a] -> [a]
++ Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
Ms.sigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup [(TyCon, Located SpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs = do
  ([[(TyCon, Located SpecType)]] -> [(TyCon, Located SpecType)])
-> Either [Error] [[(TyCon, Located SpecType)]]
-> Lookup [(TyCon, Located SpecType)]
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, Located SpecType)]] -> [(TyCon, Located SpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either [Error] [[(TyCon, Located SpecType)]]
 -> Lookup [(TyCon, Located SpecType)])
-> Either [Error] [[(TyCon, Located SpecType)]]
-> Lookup [(TyCon, Located SpecType)]
forall a b. (a -> b) -> a -> b
$
    [(ModName, DataDecl)]
-> ((ModName, DataDecl) -> Lookup [(TyCon, Located SpecType)])
-> Either [Error] [[(TyCon, Located SpecType)]]
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, Located SpecType)])
 -> Either [Error] [[(TyCon, Located SpecType)]])
-> ((ModName, DataDecl) -> Lookup [(TyCon, Located SpecType)])
-> Either [Error] [[(TyCon, Located SpecType)]]
forall a b. (a -> b) -> a -> b
$ (ModName -> DataDecl -> Lookup [(TyCon, Located SpecType)])
-> (ModName, DataDecl) -> Lookup [(TyCon, Located SpecType)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Env
-> SigEnv
-> ModName
-> DataDecl
-> Lookup [(TyCon, Located SpecType)]
makeNewType Env
env SigEnv
sigEnv)
  where
    nameDecls :: [(ModName, DataDecl)]
nameDecls = [(ModName
name, DataDecl
d) | (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) <- [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs, DataDecl
d <- Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.newtyDecls Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec]

makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl ->
               Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewType :: Env
-> SigEnv
-> ModName
-> DataDecl
-> Lookup [(TyCon, Located SpecType)]
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, Located SpecType)] -> Lookup [(TyCon, Located SpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, Located SpecType
lst)]
    Maybe TyCon
_       -> [(TyCon, Located SpecType)] -> Lookup [(TyCon, Located SpecType)]
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 :: Located SpecType
lst                       = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt
    bt :: Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt                        = DataName
-> SourcePos
-> [DataCtorP
      (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> Maybe
     [DataCtorP (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [DataCtorP
      (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl
-> Maybe
     [DataCtorP (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs = SpData
  { gsCtors :: [(Var, Located SpecType)]
gsCtors      = [Char] -> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"GS-CTORS"
                   [ (Var
x, if Bool
allowTC then Located SpecType
t else Located SpecType
tt)
                       | (Var
x, Located SpecType
t) <- MeasEnv -> [(Var, Located SpecType)]
Bare.meDataCons MeasEnv
measEnv
                       , let tt :: Located SpecType
tt  = Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
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 (Var -> PlugTV Var
forall v. v -> PlugTV v
Bare.LqTV Var
x) Located SpecType
t
                   ]
  , gsMeas :: [(Symbol, Located SpecType)]
gsMeas       = [ (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, RRType (ReftBV Symbol Symbol) -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RRType (ReftBV Symbol Symbol) -> SpecType)
-> Located (RRType (ReftBV Symbol Symbol)) -> Located SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (RRType (ReftBV Symbol Symbol))
t) | (Symbol
x, Located (RRType (ReftBV Symbol Symbol))
t) <- [(Symbol, Located (RRType (ReftBV Symbol 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 :: [Var]
gsOpaqueRefls = (Var,
 Measure
   (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
   (Located LHName))
-> Var
forall a b. (a, b) -> a
fst ((Var,
  Measure
    (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    (Located LHName))
 -> Var)
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))]
-> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv
-> [(Var,
     Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName))]
Bare.meOpaqueRefl MeasEnv
measEnv
  , gsInvariants :: [(Maybe Var, Located SpecType)]
gsInvariants = ((Maybe Var, Located SpecType) -> SourcePos)
-> [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (Located SpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located SpecType -> SourcePos)
-> ((Maybe Var, Located SpecType) -> Located SpecType)
-> (Maybe Var, Located SpecType)
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Var, Located SpecType) -> Located SpecType
forall a b. (a, b) -> b
snd) [(Maybe Var, Located SpecType)]
invs
  , gsIaliases :: [(Located SpecType, Located SpecType)]
gsIaliases   = ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [(Located SpecType, Located SpecType)])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Located SpecType, Located SpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Located SpecType, Located SpecType)]
makeIAliases Env
env SigEnv
sigEnv) (HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs)
  , gsUnsorted :: [UnSortedExpr]
gsUnsorted   = [UnSortedExpr]
usI [UnSortedExpr] -> [UnSortedExpr] -> [UnSortedExpr]
forall a. [a] -> [a] -> [a]
++ (Measure
   (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
   (Located LHName)
 -> [UnSortedExpr])
-> [Measure
      (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
      (Located LHName)]
-> [UnSortedExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure
  (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
  (Located LHName)
-> [UnSortedExpr]
forall v ty ctor. MeasureV v ty ctor -> [UnSortedExpr]
msUnSorted ((Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> [Measure
       (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
       (Located LHName)])
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [Measure
      (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
      (Located LHName)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [Measure
      (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
      (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs)
  }
  where
    allowTC :: Bool
allowTC      = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)
    measVars :: [(Symbol, Located (RRType (ReftBV Symbol Symbol)))]
measVars     = Env
-> MeasEnv -> [(Symbol, Located (RRType (ReftBV Symbol 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec       = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> ModName
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a. Monoid a => a
mempty ModName
name HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs
    name :: ModName
name         = GhcSrc -> ModName
_giTargetMod      GhcSrc
src
    ([(Maybe Var, Located SpecType)]
minvs,[UnSortedExpr]
usI)  = GhcSpecSig
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> ([(Maybe Var, Located SpecType)], [UnSortedExpr])
makeMeasureInvariants GhcSpecSig
sig Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec
    invs :: [(Maybe Var, Located SpecType)]
invs         = [(Maybe Var, Located SpecType)]
minvs [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ ((ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [(Maybe Var, Located SpecType)])
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Maybe Var, Located SpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Maybe Var, Located SpecType)]
makeInvariants Env
env SigEnv
sigEnv) (HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs)

makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases :: Env
-> SigEnv
-> (ModName,
    Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Located SpecType, Located SpecType)]
makeIAliases Env
env SigEnv
sigEnv (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec)
  = [ (Located SpecType, Located SpecType)
z | Right (Located SpecType, Located SpecType)
z <- (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Either [Error] (Located SpecType, Located SpecType)
mkIA ((Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Either [Error] (Located SpecType, Located SpecType))
-> [(Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [Either [Error] (Located SpecType, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
Ms.ialiases Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec ]
  where
    -- mkIA :: (LocBareType, LocBareType) -> Either _ (LocSpecType, LocSpecType)
    mkIA :: (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)),
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Either [Error] (Located SpecType, Located SpecType)
mkIA (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t1, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t2) = (,) (Located SpecType
 -> Located SpecType -> (Located SpecType, Located SpecType))
-> Either [Error] (Located SpecType)
-> Either
     [Error] (Located SpecType -> (Located SpecType, Located SpecType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (Located SpecType)
mkI' Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t1 Either
  [Error] (Located SpecType -> (Located SpecType, Located SpecType))
-> Either [Error] (Located SpecType)
-> Either [Error] (Located SpecType, Located SpecType)
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (Located SpecType)
mkI' Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
t2
    mkI' :: Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (Located SpecType)
mkI'          = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Either [Error] (Located SpecType)
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Maybe Var, Located SpecType)]
makeInvariants Env
env SigEnv
sigEnv (ModName
name, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec) =
  [ (Maybe Var
forall a. Maybe a
Nothing, Located SpecType
t)
    | (Maybe (Located Symbol)
_, Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt) <- Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Maybe (Located Symbol),
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall lname ty.
Spec lname ty -> [(Maybe (Located Symbol), Located ty)]
Ms.invariants Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
    , Env
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Bool
Bare.knownGhcType Env
env Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt
    , let t :: Located SpecType
t = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
bt
  ] [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++
  [[(Maybe Var, Located SpecType)]]
-> [(Maybe Var, Located SpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Maybe Var
forall a. Maybe a
Nothing,) (Located SpecType -> (Maybe Var, Located SpecType))
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> (Maybe Var, Located SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Located SpecType -> Located SpecType
makeSizeInv Symbol
l (Located SpecType -> (Maybe Var, Located SpecType))
-> [Located SpecType] -> [(Maybe Var, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  [Located SpecType]
ts
    | ([Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
bts, Symbol
l) <- Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [([Located
        (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))],
     Symbol)]
forall lname ty. Spec lname ty -> [([Located ty], lname)]
Ms.dsize Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
    , (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> Bool)
-> [Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Bool
Bare.knownGhcType Env
env) [Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
bts
    , let ts :: [Located SpecType]
ts = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> Located SpecType)
-> [Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [Located SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
bts
  ]

makeSizeInv :: F.Symbol -> Located SpecType -> Located SpecType
makeSizeInv :: Symbol -> Located SpecType -> Located SpecType
makeSizeInv Symbol
s Located SpecType
lst = Located SpecType
lst{val = go (val lst)}
  where go :: RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
go (RApp c
c [RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
ts [RTPropBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
rs UReftBV b v (ReftBV Symbol Symbol)
r) = c
-> [RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
-> [RTPropBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
-> UReftBV b v (ReftBV Symbol Symbol)
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp c
c [RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
ts [RTPropBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))]
rs (UReftBV b v (ReftBV Symbol Symbol)
r UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
forall r. Meet r => r -> r -> r
`meet` UReftBV b v (ReftBV Symbol Symbol)
forall {b} {v}.
(Monoid (PredicateBV b v), Eq b) =>
UReftBV b v (ReftBV Symbol Symbol)
nat)
        go (RAllT RTVUBV b v c tv
a RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
t UReftBV b v (ReftBV Symbol Symbol)
r)    = RTVUBV b v c tv
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
-> UReftBV b v (ReftBV Symbol Symbol)
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV b v c tv
a (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
go RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
t) UReftBV b v (ReftBV Symbol Symbol)
r
        go RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
t = RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
t
        nat :: UReftBV b v (ReftBV Symbol Symbol)
nat  = ReftBV Symbol Symbol
-> PredicateBV b v -> UReftBV b v (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
Reft (Symbol
vv_, Brel
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
PAtom Brel
Le (Constant -> ExprBV Symbol Symbol
forall b v. Constant -> ExprBV b v
ECon (Constant -> ExprBV Symbol Symbol)
-> Constant -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0) (ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
EApp (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
s) (Symbol -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
eVar Symbol
vv_))))
                       PredicateBV b v
forall a. Monoid a => a
mempty

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

measureTypeToInv :: (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv :: (Located LHName, (Var, Located SpecType))
-> ((Maybe Var, Located SpecType), Maybe UnSortedExpr)
measureTypeToInv (Located LHName
x, (Var
v, Located SpecType
t))
  = [Char]
-> ((Maybe Var, Located SpecType), Maybe UnSortedExpr)
-> ((Maybe Var, Located SpecType), Maybe UnSortedExpr)
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"measureTypeToInv" ((Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v, Located SpecType
t {val = mtype}), Maybe UnSortedExpr
usorted)
  where
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
trep = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t)
    rts :: [SpecType]
rts  = RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
-> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
trep
    args :: [Symbol]
args = RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol) -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
trep
    res :: SpecType
res  = RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol) -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res   RTypeRepBV Symbol Symbol RTyCon RTyVar (RReftV Symbol)
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}. RTypeBV Symbol Symbol c tv r -> Bool
isSimpleADT SpecType
tz then
        Maybe UnSortedExpr
forall a. Maybe a
Nothing
      else
        (Symbol -> [Symbol])
-> (Symbol, ExprBV Symbol Symbol) -> 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, ExprBV Symbol Symbol) -> UnSortedExpr)
-> Maybe (Symbol, ExprBV Symbol Symbol) -> Maybe UnSortedExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
-> Symbol
-> SpecType
-> SpecType
-> Maybe (Symbol, ExprBV Symbol Symbol)
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
$ Var -> Located LHName
makeGHCLHNameLocatedFromId Var
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
$ Located SpecType -> SourcePos
forall a. Located a -> SourcePos
loc Located SpecType
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 :: RTypeBV Symbol Symbol c tv r -> Bool
isSimpleADT (RApp c
_ [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
_ r
_) = (RTypeBV Symbol Symbol c tv r -> Bool)
-> [RTypeBV Symbol Symbol c tv r] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RTypeBV Symbol Symbol c tv r -> Bool
forall {c} {tv} {r}. RTypeBV Symbol Symbol c tv r -> Bool
isRVar [RTypeBV Symbol Symbol c tv r]
ts
    isSimpleADT RTypeBV Symbol 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 -> RReftV Symbol -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
strengthen (RReftV Symbol -> RReftV Symbol
forall r. Top r => r -> r
top (RReftV Symbol -> RReftV Symbol) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReftV Symbol
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
reft' PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty)
      where
        reft' :: ReftBV Symbol Symbol
reft' = ReftBV Symbol Symbol
-> ((Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol)
-> Maybe (Symbol, ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe ReftBV Symbol Symbol
forall a. Monoid a => a
mempty (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
Reft Maybe (Symbol, ExprBV Symbol Symbol)
mreft
        mreft :: Maybe (Symbol, ExprBV Symbol Symbol)
mreft = Located LHName
-> Symbol
-> SpecType
-> SpecType
-> Maybe (Symbol, ExprBV Symbol Symbol)
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, ExprBV Symbol Symbol)
mkReft Located LHName
x Symbol
z SpecType
_t SpecType
tr
  | Just RReftV Symbol
q <- SpecType -> Maybe (RReftV Symbol)
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase SpecType
tr
  = let Reft (ReftBind (RReftV Symbol)
v, ExprBV (ReftBind (RReftV Symbol)) (ReftVar (RReftV Symbol))
p) = RReftV Symbol
-> ReftBV (ReftBind (RReftV Symbol)) (ReftVar (RReftV Symbol))
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft RReftV Symbol
q
        su :: SubstV Symbol
su          = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
mkSubst [(Symbol
v, Located Symbol -> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall v b. Located v -> [ExprBV b v] -> ExprBV b v
mkEApp ((LHName -> Symbol) -> Located LHName -> Located Symbol
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 -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
v]), (Symbol
z,Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
v)]
        -- p'          = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p
    in  (Symbol, ExprBV Symbol Symbol)
-> Maybe (Symbol, ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (Symbol
v, SubstV (Variable (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
subst SubstV Symbol
SubstV (Variable (ExprBV Symbol Symbol))
su ExprBV Symbol Symbol
p)
mkReft Located LHName
_ Symbol
_ SpecType
_ SpecType
_
  = Maybe (Symbol, ExprBV Symbol Symbol)
forall a. Maybe a
Nothing


-- REBARE: formerly, makeGhcSpec3
-------------------------------------------------------------------------------------------
makeSpecName :: Bare.TycEnv -> Bare.MeasEnv -> [Ghc.Id] -> GhcSpecNames
-------------------------------------------------------------------------------------------
makeSpecName :: TycEnv -> MeasEnv -> [Var] -> GhcSpecNames
makeSpecName TycEnv
tycEnv MeasEnv
measEnv [Var]
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 :: [Var]
gsDataConIds = [Var]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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 :: [(Var, Located SpecType)]
tcSelVars     = [(Var, Located SpecType)]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs
    specs :: [(ModName,
  Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
specs         = (ModName
myName, Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
mySpec) (ModName,
 Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. a -> [a] -> [a]
: HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(ModName,
     Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
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) = TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
Bare.makeDataDecls 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 -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> TcRn TycEnv
makeTycEnv1 Env
env (TycEnv
tycEnv, [Located DataConP]
datacons) CoreExpr -> ExprBV Symbol Symbol
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 -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (DataConP, DataConP)
Bare.elaborateClassDcp CoreExpr -> ExprBV Symbol Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let recSelectors = Env -> [Located DataConP] -> [(Var, Located SpecType)]
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs = do
  (cls, mts)  <- Env
-> SigEnv
-> ModName
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Lookup ([DataConP], [(ModName, Var, Located SpecType)])
Bare.makeClasses        Env
env SigEnv
sigEnv ModName
name HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs
  let dms      = Env
-> [(ModName, Var, Located SpecType)]
-> [(ModName, Var, Located SpecType)]
Bare.makeDefaultMethods Env
env [(ModName, Var, Located SpecType)]
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 (ReftBV Symbol 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 (ReftBV Symbol Symbol))
-> RRType (ReftBV Symbol Symbol)
forall ty. CMeasure ty -> ty
cSort CMeasure (RRType (ReftBV Symbol Symbol))
t RRType (ReftBV Symbol Symbol)
-> Located LHName -> Located (RRType (ReftBV Symbol 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 (ReftBV Symbol Symbol))
t) <- [(Located LHName, CMeasure (RRType (ReftBV Symbol Symbol)))]
cms ]
  let ms'      = [ (LHName -> Symbol
lhNameToResolvedSymbol (Located LHName -> LHName
forall a. Located a -> a
F.val Located LHName
lx), Located LHName
-> RRType (ReftBV Symbol Symbol)
-> Located (RRType (ReftBV Symbol Symbol))
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
lx RRType (ReftBV Symbol Symbol)
t)
                 | (Located LHName
lx, RRType (ReftBV Symbol Symbol)
t) <- [(Located LHName, RRType (ReftBV Symbol Symbol))]
ms
                 , Maybe (Located (RRType (ReftBV Symbol Symbol))) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (LHName
-> [(LHName, Located (RRType (ReftBV Symbol Symbol)))]
-> Maybe (Located (RRType (ReftBV Symbol 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 (ReftBV Symbol Symbol)))]
cms')
                 ]
  let cs'      = [ (Var
v, Var -> SpecType -> Located SpecType
forall {b}. NamedThing b => b -> SpecType -> Located SpecType
txRefs Var
v SpecType
t) | (Var
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(Var, SpecType)]
-> [DataConP]
-> [(Var, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(Var, 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 -> Located SpecType
txRefs b
v SpecType
t    = TyConMap -> TCEmb TyCon -> Located SpecType -> Located SpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t SpecType -> Located b -> Located SpecType
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> MeasEnv
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Var, Located SpecType, Equation)]
-> Lookup MeasEnv
addOpaqueReflMeas Config
cfg TycEnv
tycEnv Env
env Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec MeasEnv
measEnv HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs [(Var, Located SpecType, 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [DataDecl]
-> [(Located LHName, [Variance])]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes'' Env
env ModName
name Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (ReftBV Symbol Symbol)
-> Located (RRType (ReftBV Symbol Symbol))
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
lx RRType (ReftBV Symbol Symbol)
t) | (Located LHName
lx, RRType (ReftBV Symbol Symbol)
t) <- [(Located LHName, RRType (ReftBV Symbol Symbol))]
ms ]
  let cs'      = [ (Var
v, Var -> SpecType -> Located SpecType
forall {b}. NamedThing b => b -> SpecType -> Located SpecType
txRefs Var
v SpecType
t) | (Var
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(Var, SpecType)]
-> [DataConP]
-> [(Var, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(Var, 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 -> Located SpecType
txRefs b
v SpecType
t    = TyConMap -> TCEmb TyCon -> Located SpecType -> Located SpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t SpecType -> Located b -> Located SpecType
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, [(Var,
  Measure
    (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    ctor)]
opaqueRefl) = Env
-> MeasEnv
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Var, Located SpecType, Equation)]
-> ([MSpec SpecType DataCon],
    [(Var,
      Measure
        (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
        ctor)])
forall ctor.
Env
-> MeasEnv
-> HashMap
     ModName
     (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [(Var, Located SpecType, Equation)]
-> ([MSpec SpecType DataCon],
    [(Var,
      Measure
        (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
        ctor)])
Bare.makeOpaqueReflMeasures Env
env MeasEnv
measEnv HashMap
  ModName
  (Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
specs [(Var, Located SpecType, 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. 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
spec
    shouldBeUsedForScanning :: LHName -> Bool
shouldBeUsedForScanning LHName
sym = Bool -> Bool
not (LHName
sym LHName -> HashSet LHName -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet LHName
actualFns)
    varsUsedForTcScanning :: [Var]
varsUsedForTcScanning =
      [ Var
v
      | (Var
v, Located SpecType
_, Equation
_) <- [(Var, Located SpecType, Equation)]
eqs
      , LHName -> Bool
shouldBeUsedForScanning (LHName -> Bool) -> LHName -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Symbol -> LHName
makeGHCLHName (Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName Var
v) (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
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 => (a -> b) -> HashSet a -> HashSet b
`S.map` MeasEnv -> [Var] -> HashSet DataCon
Bare.getReflDCs MeasEnv
measEnv [Var]
varsUsedForTcScanning
    dataDecls :: [DataDecl]
dataDecls     = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> [TyCon] -> [DataDecl]
Bare.makeHaskellDataDecls Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Spec
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
lSpec0 = Spec Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
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.ealiases   = M.elems . exprAliases $ myRTE
  , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
  }
  where
    myDCs :: [(Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
myDCs         = ((Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> Bool)
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a. (a -> Bool) -> [a] -> [a]
filter (LHName -> Bool
isLocalName (LHName -> Bool)
-> ((Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> LHName)
-> (Located LHName,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> 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 (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
    -> Located LHName)
-> (Located LHName,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName,
 Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> Located LHName
forall a b. (a, b) -> a
fst) ([(Located LHName,
   Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
 -> [(Located LHName,
      Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))])
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall a b. (a -> b) -> a -> b
$ [(Var, Located SpecType)]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall {f :: * -> *}.
Functor f =>
[(Var, f SpecType)]
-> [(Located LHName,
     f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
mkSigs (GhcSpecData -> [(Var, Located SpecType)]
gsCtors GhcSpecData
sData)
    mkSigs :: [(Var, f SpecType)]
-> [(Located LHName,
     f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
mkSigs [(Var, f SpecType)]
xts    = [ (Var, f SpecType)
-> (Located LHName,
    f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall {f :: * -> *}.
Functor f =>
(Var, f SpecType)
-> (Located LHName,
    f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
toBare (Var
x, f SpecType
t) | (Var
x, f SpecType
t) <- [(Var, f SpecType)]
xts
                    , Bool -> Bool
not (Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Var
x HashSet Var
reflVars) Bool -> Bool -> Bool
&& TargetSrc -> Var -> Bool
isExportedVar (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src) Var
x
                    ]
    toBare :: (Var, f SpecType)
-> (Located LHName,
    f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
toBare (Var
x, f SpecType
t) = (Var -> Located LHName
makeGHCLHNameLocatedFromId Var
x, SpecType -> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
Bare.specToBare (SpecType -> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> f SpecType
-> f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
    xbs :: [(Located LHName,
  Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
xbs           = (Var, Located SpecType)
-> (Located LHName,
    Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall {f :: * -> *}.
Functor f =>
(Var, f SpecType)
-> (Located LHName,
    f (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
toBare ((Var, Located SpecType)
 -> (Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
-> [(Var, Located SpecType)]
-> [(Located LHName,
     Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Located SpecType)]
reflTySigs
    reflTySigs :: [(Var, Located SpecType)]
reflTySigs    = [(Var
x, Located SpecType
t) | (Var
x,Located SpecType
t,Equation
_) <- GhcSpecRefl -> [(Var, Located SpecType, Equation)]
gsHAxioms GhcSpecRefl
refl]
    reflVars :: HashSet Var
reflVars      = [Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList ((Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, Located SpecType) -> Var)
-> [(Var, Located SpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Located SpecType)]
reflTySigs)
    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@ "cooks" the type aliases by converting them to SpecType and then
--   back to BareType.
--------------------------------------------------------------------------------
myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv :: GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv = BareRTEnv
rtEnv { typeAliases = M.fromList [ (aName a, a) | a <- tAs' ] }
  where
    tAs' :: [RTAlias
   Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
tAs'  = Env
-> SigEnv
-> ModName
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
normalizeBareAlias Env
env SigEnv
sigEnv ModName
modName (RTAlias
   Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
-> [RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTAlias
   Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
tAs
    tAs :: [RTAlias
   Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
tAs   = HashMap
  LHName
  (RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> [RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall k v. HashMap k v -> [v]
M.elems (HashMap
   LHName
   (RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
 -> [RTAlias
       Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))])
-> (BareRTEnv
    -> HashMap
         LHName
         (RTAlias
            Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))))
-> BareRTEnv
-> [RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv
-> HashMap
     LHName
     (RTAlias
        Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
forall tv t. RTEnv tv t -> HashMap LHName (RTAlias tv t)
typeAliases (BareRTEnv
 -> [RTAlias
       Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))])
-> BareRTEnv
-> [RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))]
forall a b. (a -> b) -> a -> b
$ BareRTEnv
rtEnv
    modName :: ModName
modName  = GhcSrc -> ModName
_giTargetMod GhcSrc
src
    aName :: RTAlias x a -> LHName
aName = Located LHName -> LHName
forall a. Located a -> a
F.val (Located LHName -> LHName)
-> (RTAlias x a -> Located LHName) -> RTAlias x a -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName

-- | Prepare an alias for constraint checking by /fixing/ its body and type argument names.
normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> BareRTAlias
                   -> BareRTAlias
normalizeBareAlias :: Env
-> SigEnv
-> ModName
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
a = RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
fixRTA RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
a
  where
    fixRTA  :: BareRTAlias -> BareRTAlias
    fixRTA :: RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
fixRTA  = (Symbol -> Symbol)
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b ty. (a -> b) -> RTAlias a ty -> RTAlias b ty
mapRTAVars Symbol -> Symbol
fixArg (RTAlias
   Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> (RTAlias
      Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
    -> RTAlias
         Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
 -> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> RTAlias
     Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
fixBody

    -- | Uses GHC to assign arguments a unique symbol by lifting them as local 'Type' variables and back.
    fixArg  :: Symbol -> Symbol
    fixArg :: Symbol -> Symbol
fixArg  = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> (Symbol -> Var) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Var
GM.symbolTyVar

    -- | Completely /cooks/ the body of a type alias by conversion to 'SpecType'
    -- and back. At this point they have been expanded already.
    fixBody :: BareType -> BareType
    fixBody :: RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
fixBody = SpecType -> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
Bare.specToBare
            (SpecType -> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
    -> SpecType)
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located SpecType -> SpecType
forall a. Located a -> a
F.val
            (Located SpecType -> SpecType)
-> (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
    -> Located SpecType)
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located SpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.RawTV
            (Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
 -> Located SpecType)
-> (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
    -> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)))
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName
-> RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol)
-> Located (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
forall l b. Loc l => l -> b -> Located b
F.atLoc (RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
-> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias
  Symbol (RTypeBV Symbol Symbol BTyCon BTyVar (RReftV Symbol))
a)


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)