{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE OverloadedStrings         #-}

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

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

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

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

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

loadLiftedSpec :: Config -> FilePath -> IO (Maybe Ms.BareSpec)
loadLiftedSpec :: Config -> FilePath -> IO (Maybe BareSpec)
loadLiftedSpec Config
cfg FilePath
srcF
  | Config -> Bool
noLiftedImport Config
cfg = FilePath -> IO ()
putStrLn FilePath
"No LIFTED Import" IO () -> IO (Maybe BareSpec) -> IO (Maybe BareSpec)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe BareSpec -> IO (Maybe BareSpec)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe BareSpec
forall a. Maybe a
Nothing 
  | Bool
otherwise          = do
      let specF :: FilePath
specF = Ext -> FilePath -> FilePath
extFileName Ext
BinSpec FilePath
srcF
      Bool
ex  <- FilePath -> IO Bool
doesFileExist FilePath
specF
      IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Loading Binary Lifted Spec: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
specF FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"for source-file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
srcF FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Bool -> FilePath
forall a. Show a => a -> FilePath
show Bool
ex
      Maybe BareSpec
lSp <- if Bool
ex 
               then BareSpec -> Maybe BareSpec
forall a. a -> Maybe a
Just (BareSpec -> Maybe BareSpec) -> IO BareSpec -> IO (Maybe BareSpec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO BareSpec
forall a. Binary a => FilePath -> IO a
B.decodeFile FilePath
specF 
               else (FilePath -> FilePath -> IO ()
warnMissingLiftedSpec FilePath
srcF FilePath
specF IO () -> IO (Maybe BareSpec) -> IO (Maybe BareSpec)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe BareSpec -> IO (Maybe BareSpec)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe BareSpec
forall a. Maybe a
Nothing)
      Maybe BareSpec -> IO (Maybe BareSpec)
forall a. a -> IO a
Ex.evaluate Maybe BareSpec
lSp

warnMissingLiftedSpec :: FilePath -> FilePath -> IO () 
warnMissingLiftedSpec :: FilePath -> FilePath -> IO ()
warnMissingLiftedSpec FilePath
srcF FilePath
specF = do 
  FilePath
incDir <- IO FilePath
Misc.getIncludeDir 
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FilePath -> FilePath -> Bool
Misc.isIncludeFile FilePath
incDir FilePath
srcF)
    (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ UserError -> IO ()
forall a e. Exception e => e -> a
Ex.throw (FilePath -> FilePath -> UserError
errMissingSpec FilePath
srcF FilePath
specF) 

errMissingSpec :: FilePath -> FilePath -> UserError 
errMissingSpec :: FilePath -> FilePath -> UserError
errMissingSpec FilePath
srcF FilePath
specF = SrcSpan -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrNoSpec SrcSpan
Ghc.noSrcSpan (FilePath -> Doc
text FilePath
srcF) (FilePath -> Doc
text FilePath
specF)

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

{- $creatingTargetSpecs

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

-- | 'makeTargetSpec' constructs the 'TargetSpec' and then validates it. Upon success, the 'TargetSpec'
-- and the 'LiftedSpec' are returned. We perform error checking in \"two phases\": during the first phase,
-- we check for errors and warnings in the input 'BareSpec' and the dependencies. During this phase we ideally
-- want to short-circuit in case the validation failure is found in one of the dependencies (to avoid
-- printing potentially endless failures).
-- The second phase involves creating the 'TargetSpec', and returning either the full list of diagnostics
-- (errors and warnings) in case things went wrong, or the final 'TargetSpec' and 'LiftedSpec' together
-- with a list of 'Warning's, which shouldn't abort the compilation (modulo explicit request from the user,
-- to treat warnings and errors).
makeTargetSpec :: Config
               -> LogicMap
               -> TargetSrc
               -> BareSpec
               -> TargetDependencies
               -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
makeTargetSpec :: Config
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
makeTargetSpec Config
cfg LogicMap
lmap TargetSrc
targetSrc BareSpec
bareSpec TargetDependencies
dependencies = do
  let depsDiagnostics :: Either Diagnostics [()]
depsDiagnostics     = ((ModName, BareSpec) -> Either Diagnostics ())
-> [(ModName, BareSpec)] -> Either Diagnostics [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((ModName -> BareSpec -> Either Diagnostics ())
-> (ModName, BareSpec) -> Either Diagnostics ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName -> BareSpec -> Either Diagnostics ()
Bare.checkBareSpec) [(ModName, BareSpec)]
legacyDependencies
  let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = ModName -> BareSpec -> Either Diagnostics ()
Bare.checkBareSpec (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc) BareSpec
legacyBareSpec
  case Either Diagnostics [()]
depsDiagnostics Either Diagnostics [()]
-> Either Diagnostics () -> Either Diagnostics ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics ()
bareSpecDiagnostics of
   Left Diagnostics
d | Diagnostics -> Bool
noErrors Diagnostics
d -> [Warning] -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
secondPhase (Diagnostics -> [Warning]
allWarnings Diagnostics
d)
   Left Diagnostics
d              -> Diagnostics
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a b. a -> Either a b
Left  Diagnostics
d
   Right ()            -> [Warning] -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
secondPhase [Warning]
forall a. Monoid a => a
mempty
  where
    secondPhase :: [Warning] -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
    secondPhase :: [Warning] -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
secondPhase [Warning]
phaseOneWarns = do
      ([Warning]
warns, GhcSpec
ghcSpec) <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, BareSpec)]
-> Either Diagnostics ([Warning], GhcSpec)
makeGhcSpec Config
cfg (Optic' An_Iso NoIx GhcSrc TargetSrc -> TargetSrc -> GhcSrc
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' An_Iso NoIx GhcSrc TargetSrc
targetSrcIso TargetSrc
targetSrc) LogicMap
lmap (BareSpec -> [(ModName, BareSpec)]
allSpecs BareSpec
legacyBareSpec)
      let (TargetSpec
targetSpec, LiftedSpec
liftedSpec) = Optic' A_Getter NoIx GhcSpec (TargetSpec, LiftedSpec)
-> GhcSpec -> (TargetSpec, LiftedSpec)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Getter NoIx GhcSpec (TargetSpec, LiftedSpec)
targetSpecGetter GhcSpec
ghcSpec
      ([Warning], TargetSpec, LiftedSpec)
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
phaseOneWarns [Warning] -> [Warning] -> [Warning]
forall a. Semigroup a => a -> a -> a
<> [Warning]
warns, TargetSpec
targetSpec, LiftedSpec
liftedSpec)

    toLegacyDep :: (StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
    toLegacyDep :: (StableModule, LiftedSpec) -> (ModName, BareSpec)
toLegacyDep (StableModule
sm, LiftedSpec
ls) = (ModType -> ModuleName -> ModName
ModName ModType
SrcImport (Module -> ModuleName
Ghc.moduleName (Module -> ModuleName)
-> (StableModule -> Module) -> StableModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> Module
unStableModule (StableModule -> ModuleName) -> StableModule -> ModuleName
forall a b. (a -> b) -> a -> b
$ StableModule
sm), LiftedSpec -> BareSpec
unsafeFromLiftedSpec LiftedSpec
ls)

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

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

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

    legacyBareSpec :: Spec LocBareType F.LocSymbol
    legacyBareSpec :: BareSpec
legacyBareSpec = Optic' An_Iso NoIx BareSpec BareSpec -> BareSpec -> BareSpec
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' An_Iso NoIx BareSpec BareSpec
bareSpecIso BareSpec
bareSpec

-------------------------------------------------------------------------------------
-- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
--   validates it using @checkGhcSpec@.
-------------------------------------------------------------------------------------
makeGhcSpec :: Config
            -> GhcSrc
            -> LogicMap
            -> [(ModName, Ms.BareSpec)]
            -> Either Diagnostics ([Warning], GhcSpec)
-------------------------------------------------------------------------------------
makeGhcSpec :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, BareSpec)]
-> Either Diagnostics ([Warning], GhcSpec)
makeGhcSpec Config
cfg GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
validatedSpecs = do
  case Either Diagnostics ()
diagnostics of
    Left Diagnostics
e | Diagnostics -> Bool
noErrors Diagnostics
e -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics -> [Warning]
allWarnings Diagnostics
e, GhcSpec
sp)
    Left Diagnostics
e              -> Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
e
    Right ()            -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
forall a. Monoid a => a
mempty, GhcSpec
sp)
  where
    diagnostics :: Either Diagnostics ()
diagnostics = [BareSpec]
-> TargetSrc
-> SEnv SortedReft
-> [CoreBind]
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (((ModName, BareSpec) -> BareSpec)
-> [(ModName, BareSpec)] -> [BareSpec]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd [(ModName, BareSpec)]
validatedSpecs)
                                       (Optic' An_Iso NoIx GhcSrc TargetSrc -> GhcSrc -> TargetSrc
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' An_Iso NoIx GhcSrc TargetSrc
targetSrcIso GhcSrc
src)
                                       SEnv SortedReft
renv
                                       [CoreBind]
cbs
                                       ((TargetSpec, LiftedSpec) -> TargetSpec
forall a b. (a, b) -> a
fst ((TargetSpec, LiftedSpec) -> TargetSpec)
-> (GhcSpec -> (TargetSpec, LiftedSpec)) -> GhcSpec -> TargetSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Getter NoIx GhcSpec (TargetSpec, LiftedSpec)
-> GhcSpec -> (TargetSpec, LiftedSpec)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Getter NoIx GhcSpec (TargetSpec, LiftedSpec)
targetSpecGetter (GhcSpec -> TargetSpec) -> GhcSpec -> TargetSpec
forall a b. (a -> b) -> a -> b
$ GhcSpec
sp)
    sp :: GhcSpec
sp          = Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> GhcSpec
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
validatedSpecs
    renv :: SEnv SortedReft
renv        = GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp
    cbs :: [CoreBind]
cbs         = GhcSrc -> [CoreBind]
_giCbs GhcSrc
src

ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol, SortedReft)]
binds
  where
    emb :: TCEmb TyCon
emb       = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp)
    binds :: [(Symbol, SortedReft)]
binds     = [[(Symbol, SortedReft)]] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 
                 [ [(Symbol
x,        RRType RReft -> SortedReft
forall r.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort RRType RReft
t) | (Symbol
x, Loc SourcePos
_ SourcePos
_ RRType RReft
t) <- GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas     (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v, RRType RReft -> SortedReft
forall r.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort RRType RReft
t) | (Var
v, Loc SourcePos
_ SourcePos
_ RRType RReft
t) <- GhcSpecData -> [(Var, LocSpecType)]
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,        Var -> SortedReft
vSort Var
v) | (Symbol
x, Var
v)         <- GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp), Var -> Bool
Ghc.isConLikeId Var
v ]
                 , [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s Reft
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)         <- [(Symbol, Sort)]
wiredSortedSyms       ]
                 , [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s Reft
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)         <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp       ]
                 ]
    vSort :: Var -> SortedReft
vSort     = TCEmb TyCon -> Var -> SortedReft
Bare.varSortedReft TCEmb TyCon
emb
    rSort :: RRType r -> SortedReft
rSort     = TCEmb TyCon -> RRType r -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft    TCEmb TyCon
emb


-------------------------------------------------------------------------------------
-- | @makeGhcSpec0@ slurps up all the relevant information needed to generate 
--   constraints for a target module and packages them into a @GhcSpec@ 
--   See [NOTE] LIFTING-STAGES to see why we split into lSpec0, lSpec1, etc.
--   essentially, to get to the `BareRTEnv` as soon as possible, as thats what
--   lets us use aliases inside data-constructor definitions.
-------------------------------------------------------------------------------------
makeGhcSpec0 :: Config -> GhcSrc ->  LogicMap -> [(ModName, Ms.BareSpec)] -> GhcSpec
-------------------------------------------------------------------------------------
makeGhcSpec0 :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> GhcSpec
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
mspecs = SP :: GhcSpecSig
-> GhcSpecQual
-> GhcSpecData
-> GhcSpecNames
-> GhcSpecVars
-> GhcSpecTerm
-> GhcSpecRefl
-> GhcSpecLaws
-> [(Symbol, Sort)]
-> Config
-> BareSpec
-> GhcSpec
SP 
  { _gsConfig :: Config
_gsConfig = Config
cfg 
  , _gsImps :: [(Symbol, Sort)]
_gsImps   = [(ModName, BareSpec)] -> [(Symbol, Sort)]
makeImports [(ModName, BareSpec)]
mspecs
  , _gsSig :: GhcSpecSig
_gsSig    = GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs GhcSpecRefl
refl GhcSpecSig
sig 
  , _gsRefl :: GhcSpecRefl
_gsRefl   = GhcSpecRefl
refl 
  , _gsLaws :: GhcSpecLaws
_gsLaws   = GhcSpecLaws
laws 
  , _gsData :: GhcSpecData
_gsData   = GhcSpecData
sData 
  , _gsQual :: GhcSpecQual
_gsQual   = GhcSpecQual
qual 
  , _gsName :: GhcSpecNames
_gsName   = Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env     TycEnv
tycEnv MeasEnv
measEnv   ModName
name 
  , _gsVars :: GhcSpecVars
_gsVars   = Config -> GhcSrc -> BareSpec -> Env -> MeasEnv -> GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src BareSpec
mySpec Env
env MeasEnv
measEnv
  , _gsTerm :: GhcSpecTerm
_gsTerm   = Config -> BareSpec -> Env -> ModName -> GhcSpecTerm
makeSpecTerm Config
cfg     BareSpec
mySpec Env
env       ModName
name    
  , _gsLSpec :: BareSpec
_gsLSpec  = BareSpec
finalLiftedSpec
              { impSigs :: [(Symbol, Sort)]
impSigs   = [(ModName, BareSpec)] -> [(Symbol, Sort)]
makeImports [(ModName, BareSpec)]
mspecs
              , expSigs :: [(Symbol, Sort)]
expSigs   = [ (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v, SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SortedReft -> Sort
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> Var -> SortedReft
Bare.varSortedReft TCEmb TyCon
embs Var
v) | Var
v <- GhcSpecRefl -> [Var]
gsReflects GhcSpecRefl
refl ]
              , dataDecls :: [DataDecl]
dataDecls = BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls BareSpec
mySpec2
              , measures :: [Measure LocBareType LocSymbol]
measures  = BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures BareSpec
mySpec
                -- We want to export measures in a 'LiftedSpec', especially if they are
                -- required to check termination of some 'liftedSigs' we export. Due to the fact
                -- that 'lSpec1' doesn't contain the measures that we compute via 'makeHaskellMeasures',
                -- we take them from 'mySpec', which has those.
              , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs = BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs BareSpec
finalLiftedSpec [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a. [a] -> [a] -> [a]
++ BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs BareSpec
mySpec
                -- Export all the assumptions (not just the ones created out of reflection) in
                -- a 'LiftedSpec'.
              , imeasures :: [Measure LocBareType LocSymbol]
imeasures = BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures BareSpec
finalLiftedSpec [Measure LocBareType LocSymbol]
-> [Measure LocBareType LocSymbol]
-> [Measure LocBareType LocSymbol]
forall a. [a] -> [a] -> [a]
++ BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures BareSpec
mySpec
                -- Preserve user-defined 'imeasures'.
              , dvariance :: [(LocSymbol, [Variance])]
dvariance = BareSpec -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance BareSpec
finalLiftedSpec [(LocSymbol, [Variance])]
-> [(LocSymbol, [Variance])] -> [(LocSymbol, [Variance])]
forall a. [a] -> [a] -> [a]
++ BareSpec -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance BareSpec
mySpec
                -- Preserve user-defined 'dvariance'.
              , rinstance :: [RInstance LocBareType]
rinstance = BareSpec -> [RInstance LocBareType]
forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance BareSpec
finalLiftedSpec [RInstance LocBareType]
-> [RInstance LocBareType] -> [RInstance LocBareType]
forall a. [a] -> [a] -> [a]
++ BareSpec -> [RInstance LocBareType]
forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance BareSpec
mySpec
                -- Preserve rinstances.
              }
  }
  where
    finalLiftedSpec :: BareSpec
finalLiftedSpec = GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> BareSpec
-> BareSpec
makeLiftedSpec GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE BareSpec
lSpec1
    -- build up spec components 
    myRTE :: BareRTEnv
myRTE    = GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv       GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv  
    qual :: GhcSpecQual
qual     = Config
-> Env -> TycEnv -> MeasEnv -> BareRTEnv -> ModSpecs -> GhcSpecQual
makeSpecQual Config
cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv ModSpecs
specs 
    sData :: GhcSpecData
sData    = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> ModSpecs
-> GhcSpecData
makeSpecData  GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig ModSpecs
specs 
    refl :: GhcSpecRefl
refl     = Config
-> GhcSrc
-> MeasEnv
-> ModSpecs
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> GhcSpecRefl
makeSpecRefl  Config
cfg GhcSrc
src MeasEnv
measEnv ModSpecs
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv 
    laws :: GhcSpecLaws
laws     = Env
-> SigEnv
-> [(Var, LocSpecType)]
-> MeasEnv
-> ModSpecs
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sig [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sig) MeasEnv
measEnv ModSpecs
specs 
    sig :: GhcSpecSig
sig      = Config
-> ModName
-> ModSpecs
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> GhcSpecSig
makeSpecSig Config
cfg ModName
name ModSpecs
specs Env
env SigEnv
sigEnv   TycEnv
tycEnv MeasEnv
measEnv (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
    measEnv :: MeasEnv
measEnv  = Env -> TycEnv -> SigEnv -> ModSpecs -> MeasEnv
makeMeasEnv      Env
env TycEnv
tycEnv SigEnv
sigEnv       ModSpecs
specs 
    -- build up environments
    specs :: ModSpecs
specs    = ModName -> BareSpec -> ModSpecs -> ModSpecs
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name BareSpec
mySpec ModSpecs
iSpecs2
    mySpec :: BareSpec
mySpec   = BareSpec
mySpec2 BareSpec -> BareSpec -> BareSpec
forall a. Semigroup a => a -> a -> a
<> BareSpec
lSpec1 
    lSpec1 :: BareSpec
lSpec1   = BareSpec
lSpec0 BareSpec -> BareSpec -> BareSpec
forall a. Semigroup a => a -> a -> a
<> Config -> GhcSrc -> TycEnv -> LogicMap -> BareSpec -> BareSpec
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap BareSpec
mySpec1 
    sigEnv :: SigEnv
sigEnv   = TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv  TCEmb TyCon
embs TyConMap
tyi (GhcSrc -> HashSet StableName
_gsExports GhcSrc
src) BareRTEnv
rtEnv 
    tyi :: TyConMap
tyi      = TycEnv -> TyConMap
Bare.tcTyConMap   TycEnv
tycEnv 
    tycEnv :: TycEnv
tycEnv   = Config
-> ModName -> Env -> TCEmb TyCon -> BareSpec -> ModSpecs -> TycEnv
makeTycEnv   Config
cfg ModName
name Env
env TCEmb TyCon
embs BareSpec
mySpec2 ModSpecs
iSpecs2 
    mySpec2 :: BareSpec
mySpec2  = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> BareSpec
-> BareSpec
forall a.
(Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] BareSpec
mySpec1    where l :: SourcePos
l = FilePath -> SourcePos
F.dummyPos FilePath
"expand-mySpec2"
    iSpecs2 :: ModSpecs
iSpecs2  = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> ModSpecs
-> ModSpecs
forall a.
(Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] ModSpecs
iSpecs0    where l :: SourcePos
l = FilePath -> SourcePos
F.dummyPos FilePath
"expand-iSpecs2"
    rtEnv :: BareRTEnv
rtEnv    = Env -> ModName -> BareSpec -> ModSpecs -> LogicMap -> BareRTEnv
Bare.makeRTEnv Env
env ModName
name BareSpec
mySpec1 ModSpecs
iSpecs0 LogicMap
lmap  
    mySpec1 :: BareSpec
mySpec1  = BareSpec
mySpec0 BareSpec -> BareSpec -> BareSpec
forall a. Semigroup a => a -> a -> a
<> BareSpec
lSpec0    
    lSpec0 :: BareSpec
lSpec0   = Config -> GhcSrc -> TCEmb TyCon -> LogicMap -> BareSpec -> BareSpec
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap BareSpec
mySpec0 
    embs :: TCEmb TyCon
embs     = GhcSrc -> Env -> [(ModName, BareSpec)] -> TCEmb TyCon
makeEmbeds          GhcSrc
src Env
env ((ModName
name, BareSpec
mySpec0) (ModName, BareSpec)
-> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
forall a. a -> [a] -> [a]
: ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
iSpecs0)
    -- extract name and specs
    env :: Env
env      = Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
Bare.makeEnv Config
cfg GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
mspecs  
    (BareSpec
mySpec0, ModSpecs
iSpecs0) = ModName -> [(ModName, BareSpec)] -> (BareSpec, ModSpecs)
splitSpecs ModName
name [(ModName, BareSpec)]
mspecs 
    -- check barespecs 
    name :: ModName
name     = FilePath -> ModName -> ModName
forall a. PPrint a => FilePath -> a -> a
F.notracepp (FilePath
"ALL-SPECS" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
zzz) (ModName -> ModName) -> ModName -> ModName
forall a b. (a -> b) -> a -> b
$ GhcSrc -> ModName
_giTargetMod  GhcSrc
src 
    zzz :: FilePath
zzz      = [ModName] -> FilePath
forall a. PPrint a => a -> FilePath
F.showpp ((ModName, BareSpec) -> ModName
forall a b. (a, b) -> a
fst ((ModName, BareSpec) -> ModName)
-> [(ModName, BareSpec)] -> [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, BareSpec)]
mspecs)

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


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


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

makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: Env -> (ModName, BareSpec) -> TCEmb TyCon
makeTyConEmbeds Env
env (ModName
name, BareSpec
spec) 
  = [(TyCon, (Sort, TCArgs))] -> TCEmb TyCon
forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (LocSymbol
c,(Sort, TCArgs)
t) <- TCEmb LocSymbol -> [(LocSymbol, (Sort, TCArgs))]
forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (BareSpec -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds BareSpec
spec), TyCon
tc <- LocSymbol -> [TyCon]
forall a. ResolveSym a => LocSymbol -> [a]
symTc LocSymbol
c ]
    where
      symTc :: LocSymbol -> [a]
symTc = Maybe a -> [a]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe a -> [a]) -> (LocSymbol -> Maybe a) -> LocSymbol -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> FilePath -> LocSymbol -> Maybe a
forall a.
ResolveSym a =>
Env -> ModName -> FilePath -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name FilePath
"embed-tycon" 

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

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

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

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

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

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

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

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

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

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv -> GhcSpecVars 
------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> BareSpec -> Env -> MeasEnv -> GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src BareSpec
mySpec Env
env MeasEnv
measEnv = SpVar :: [Var] -> HashSet Var -> HashSet Var -> [Var] -> GhcSpecVars
SpVar 
  { gsTgtVars :: [Var]
gsTgtVars    =   (FilePath -> Var) -> [FilePath] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> ModName -> FilePath -> Var
resolveStringVar  Env
env ModName
name)              (Config -> [FilePath]
checks     Config
cfg) 
  , gsIgnoreVars :: HashSet Var
gsIgnoreVars = (LocSymbol -> Var) -> HashSet LocSymbol -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"gs-ignores") (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.ignores BareSpec
mySpec) 
  , gsLvars :: HashSet Var
gsLvars      = (LocSymbol -> Var) -> HashSet LocSymbol -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"gs-lvars"  ) (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lvars   BareSpec
mySpec)
  , gsCMethods :: [Var]
gsCMethods   = (ModName, Var, LocSpecType) -> Var
forall a b c. (a, b, c) -> b
snd3 ((ModName, Var, LocSpecType) -> Var)
-> [(ModName, Var, LocSpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(ModName, Var, LocSpecType)]
Bare.meMethods MeasEnv
measEnv 
  }
  where name :: ModName
name     = GhcSrc -> ModName
_giTargetMod GhcSrc
src 

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

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

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

makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty bndr) -> [F.Qualifier]
makeQualifiers :: Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv (ModName
mod, Spec ty bndr
spec) 
  = (Qualifier -> Qualifier) -> [Qualifier] -> [Qualifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap        (Env -> ModName -> Qualifier -> Qualifier
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env        ModName
mod) 
  ([Qualifier] -> [Qualifier])
-> ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> Maybe Qualifier) -> [Qualifier] -> [Qualifier]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams       Env
env TycEnv
tycEnv ModName
mod)
  ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> [Qualifier]
forall ty bndr. Spec ty bndr -> [Qualifier]
Ms.qualifiers Spec ty bndr
spec 


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

resolveQParams :: Bare.Env -> Bare.TycEnv -> ModName -> F.Qualifier -> Maybe F.Qualifier 
resolveQParams :: Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams Env
env TycEnv
tycEnv ModName
name Qualifier
q = do 
     [QualParam]
qps   <- (QualParam -> Maybe QualParam) -> [QualParam] -> Maybe [QualParam]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QualParam -> Maybe QualParam
goQP (Qualifier -> [QualParam]
F.qParams Qualifier
q) 
     Qualifier -> Maybe Qualifier
forall (m :: * -> *) a. Monad m => a -> m a
return (Qualifier -> Maybe Qualifier) -> Qualifier -> Maybe Qualifier
forall a b. (a -> b) -> a -> b
$ Qualifier
q { qParams :: [QualParam]
F.qParams = [QualParam]
qps } 
  where 
    goQP :: QualParam -> Maybe QualParam
goQP QualParam
qp          = do { Sort
s <- Sort -> Maybe Sort
go (QualParam -> Sort
F.qpSort QualParam
qp) ; QualParam -> Maybe QualParam
forall (m :: * -> *) a. Monad m => a -> m a
return QualParam
qp { qpSort :: Sort
F.qpSort = Sort
s } } 
    go               :: F.Sort -> Maybe F.Sort   
    go :: Sort -> Maybe Sort
go (FAbs Int
i Sort
s)    = Int -> Sort -> Sort
FAbs Int
i (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Maybe Sort
go Sort
s2
    go (FTC FTycon
c)       = Env -> TycEnv -> ModName -> FTycon -> Maybe Sort
qualifyFTycon Env
env TycEnv
tycEnv ModName
name FTycon
c 
    go Sort
s             = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s 

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

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

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

------------------------------------------------------------------------------------------
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName -> GhcSpecTerm 
------------------------------------------------------------------------------------------
makeSpecTerm :: Config -> BareSpec -> Env -> ModName -> GhcSpecTerm
makeSpecTerm Config
cfg BareSpec
mySpec Env
env ModName
name = SpTerm :: HashSet Var
-> HashSet TyCon
-> HashSet Var
-> HashSet (Located Var)
-> [(Var, [Int])]
-> HashSet Var
-> GhcSpecTerm
SpTerm 
  { gsLazy :: HashSet Var
gsLazy       = Var -> HashSet Var -> HashSet Var
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Var
dictionaryVar (HashSet Var
lazies HashSet Var -> HashSet Var -> HashSet Var
forall a. Monoid a => a -> a -> a
`mappend` HashSet Var
sizes)
  , gsFail :: HashSet (Located Var)
gsFail       = Env -> ModName -> BareSpec -> HashSet (Located Var)
makeFail     Env
env ModName
name BareSpec
mySpec 
  , gsStTerm :: HashSet Var
gsStTerm     = HashSet Var
sizes
  , gsAutosize :: HashSet TyCon
gsAutosize   = HashSet TyCon
autos 
  , gsDecr :: [(Var, [Int])]
gsDecr       = Env -> ModName -> BareSpec -> [(Var, [Int])]
makeDecrs Env
env ModName
name BareSpec
mySpec
  , gsNonStTerm :: HashSet Var
gsNonStTerm  = HashSet Var
forall a. Monoid a => a
mempty 
  }
  where  
    lazies :: HashSet Var
lazies       = Env -> ModName -> BareSpec -> HashSet Var
makeLazy     Env
env ModName
name BareSpec
mySpec
    autos :: HashSet TyCon
autos        = Env -> ModName -> BareSpec -> HashSet TyCon
makeAutoSize Env
env ModName
name BareSpec
mySpec
    strT :: Bool
strT         = Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
structuralTerm Config
cfg) 
    sizes :: HashSet Var
sizes 
     | Bool
strT      = Env -> ModName -> BareSpec -> HashSet Var
makeSize Env
env ModName
name BareSpec
mySpec 
     | Bool
otherwise = HashSet Var
forall a. Monoid a => a
mempty 

-- formerly, makeHints
makeDecrs :: Bare.Env -> ModName -> Ms.BareSpec -> [(Ghc.Var, [Int])] 
makeDecrs :: Env -> ModName -> BareSpec -> [(Var, [Int])]
makeDecrs Env
env ModName
name BareSpec
mySpec = 
  [ (Var
v, [Int]
z) | (LocSymbol
lx, [Int]
z) <- BareSpec -> [(LocSymbol, [Int])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Int])]
Ms.decr BareSpec
mySpec
           , let v :: Var
v    = Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"decreasing" LocSymbol
lx
  ]

makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> S.HashSet Ghc.Var
makeLazy :: Env -> ModName -> BareSpec -> HashSet Var
makeLazy Env
env ModName
name BareSpec
spec = 
  (LocSymbol -> Var) -> HashSet LocSymbol -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var") (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lazy BareSpec
spec)

makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> S.HashSet (Located Ghc.Var)
makeFail :: Env -> ModName -> BareSpec -> HashSet (Located Var)
makeFail Env
env ModName
name BareSpec
spec = 
  (LocSymbol -> Located Var)
-> HashSet LocSymbol -> HashSet (Located Var)
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (\LocSymbol
x -> LocSymbol
x{ val :: Var
val = Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var" LocSymbol
x}) (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.fails BareSpec
spec)

makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> S.HashSet (Located Ghc.Var)
makeRewrite :: Env -> ModName -> BareSpec -> HashSet (Located Var)
makeRewrite Env
env ModName
name BareSpec
spec = 
  (LocSymbol -> Located Var)
-> HashSet LocSymbol -> HashSet (Located Var)
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (\LocSymbol
x -> LocSymbol
x{ val :: Var
val = Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var" LocSymbol
x}) (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.rewrites BareSpec
spec)

makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> M.HashMap Ghc.Var [Ghc.Var]
makeRewriteWith :: Env -> ModName -> BareSpec -> HashMap Var [Var]
makeRewriteWith Env
env ModName
name BareSpec
spec = 
  [(Var, [Var])] -> HashMap Var [Var]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (LocSymbol -> Var
lu LocSymbol
x, LocSymbol -> Var
lu (LocSymbol -> Var) -> [LocSymbol] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
xs) | (LocSymbol
x,[LocSymbol]
xs) <- HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])])
-> HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall a b. (a -> b) -> a -> b
$ BareSpec -> HashMap LocSymbol [LocSymbol]
forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
Ms.rewriteWith BareSpec
spec]
    where lu :: LocSymbol -> Var
lu = Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var"  


makeAutoSize :: Bare.Env -> ModName -> Ms.BareSpec -> S.HashSet Ghc.TyCon
makeAutoSize :: Env -> ModName -> BareSpec -> HashSet TyCon
makeAutoSize Env
env ModName
name BareSpec
spec =
  (LocSymbol -> TyCon) -> HashSet LocSymbol -> HashSet TyCon
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Env -> ModName -> FilePath -> LocSymbol -> TyCon
Bare.lookupGhcTyCon Env
env ModName
name FilePath
"TyCon") (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.autosize BareSpec
spec) 

makeSize :: Bare.Env -> ModName -> Ms.BareSpec -> S.HashSet Ghc.Var
makeSize :: Env -> ModName -> BareSpec -> HashSet Var
makeSize Env
env ModName
name BareSpec
spec = 
  (LocSymbol -> Var) -> HashSet LocSymbol -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var") ([LocSymbol] -> HashSet LocSymbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol]
lzs)
  where
    lzs :: [LocSymbol]
lzs = [Maybe LocSymbol] -> [LocSymbol]
forall a. [Maybe a] -> [a]
Mb.catMaybes (DataDecl -> Maybe LocSymbol
getSizeFuns (DataDecl -> Maybe LocSymbol) -> [DataDecl] -> [Maybe LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
spec)
    getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns DataDecl
decl
      | Just SizeFun
x       <- DataDecl -> Maybe SizeFun
tycSFun DataDecl
decl
      , SymSizeFun LocSymbol
f <- SizeFun
x
      = LocSymbol -> Maybe LocSymbol
forall a. a -> Maybe a
Just LocSymbol
f
      | Bool
otherwise
      = Maybe LocSymbol
forall a. Maybe a
Nothing

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

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

    lmap :: LogicMap
lmap         = Env -> LogicMap
Bare.reLMap Env
env

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

getReflects :: Bare.ModSpecs -> [Symbol]
getReflects :: ModSpecs -> [Symbol]
getReflects  = (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSymbol -> Symbol
forall a. Located a -> a
val ([LocSymbol] -> [Symbol])
-> (ModSpecs -> [LocSymbol]) -> ModSpecs -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet LocSymbol -> [LocSymbol])
-> (ModSpecs -> HashSet LocSymbol) -> ModSpecs -> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HashSet LocSymbol] -> HashSet LocSymbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions ([HashSet LocSymbol] -> HashSet LocSymbol)
-> (ModSpecs -> [HashSet LocSymbol])
-> ModSpecs
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, BareSpec) -> HashSet LocSymbol)
-> [(ModName, BareSpec)] -> [HashSet LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
names (BareSpec -> HashSet LocSymbol)
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd) ([(ModName, BareSpec)] -> [HashSet LocSymbol])
-> (ModSpecs -> [(ModName, BareSpec)])
-> ModSpecs
-> [HashSet LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList
  where
    names :: Spec ty bndr -> HashSet LocSymbol
names  Spec ty bndr
z = [HashSet LocSymbol] -> HashSet LocSymbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions [ Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec ty bndr
z ]
    
------------------------------------------------------------------------------------------
-- | @updateReflSpecSig@ uses the information about reflected functions to update the 
--   "assumed" signatures. 
------------------------------------------------------------------------------------------
addReflSigs :: GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
------------------------------------------------------------------------------------------
addReflSigs :: GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs GhcSpecRefl
refl GhcSpecSig
sig = GhcSpecSig
sig { gsRefSigs :: [(Var, LocSpecType)]
gsRefSigs = [(Var, LocSpecType)]
reflSigs, gsAsmSigs :: [(Var, LocSpecType)]
gsAsmSigs = [(Var, LocSpecType)]
wreflSigs [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var, LocSpecType) -> Bool
forall b. (Var, b) -> Bool
notReflected (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sig) }
  where 
    ([(Var, LocSpecType)]
wreflSigs, [(Var, LocSpecType)]
reflSigs)   = ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)]
-> ([(Var, LocSpecType)], [(Var, LocSpecType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
refl) (Var -> Bool)
-> ((Var, LocSpecType) -> Var) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) 
                                 [ (Var
x, LocSpecType
t) | (Var
x, LocSpecType
t, Equation
_) <- GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl ]   
    reflected :: [Var]
reflected       = (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, LocSpecType) -> Var) -> [(Var, LocSpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Var, LocSpecType)]
wreflSigs [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(Var, LocSpecType)]
reflSigs)
    notReflected :: (Var, b) -> Bool
notReflected (Var, b)
xt = (Var, b) -> Var
forall a b. (a, b) -> a
fst (Var, b)
xt Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Var]
reflected

makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> M.HashMap Ghc.Var (Maybe Int)
makeAutoInst :: Env -> ModName -> BareSpec -> HashMap Var (Maybe Int)
makeAutoInst Env
env ModName
name BareSpec
spec = (LocSymbol -> Var)
-> HashMap LocSymbol (Maybe Int) -> HashMap Var (Maybe Int)
forall k2 k1 v.
(Eq k2, Hashable k2) =>
(k1 -> k2) -> HashMap k1 v -> HashMap k2 v
Misc.hashMapMapKeys (Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"Var") (BareSpec -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
Ms.autois BareSpec
spec)

----------------------------------------------------------------------------------------
makeSpecSig :: Config -> ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
            -> GhcSpecSig 
----------------------------------------------------------------------------------------
makeSpecSig :: Config
-> ModName
-> ModSpecs
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> GhcSpecSig
makeSpecSig Config
cfg ModName
name ModSpecs
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [CoreBind]
cbs = SpSig :: [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(TyCon, LocSpecType)]
-> DEnv Var LocSpecType
-> [(Var, MethodType LocSpecType)]
-> [(Var, LocSpecType, [Located Expr])]
-> GhcSpecSig
SpSig 
  { gsTySigs :: [(Var, LocSpecType)]
gsTySigs   = FilePath -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"gsTySigs"  [(Var, LocSpecType)]
tySigs 
  , gsAsmSigs :: [(Var, LocSpecType)]
gsAsmSigs  = FilePath -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"gsAsmSigs" [(Var, LocSpecType)]
asmSigs
  , gsRefSigs :: [(Var, LocSpecType)]
gsRefSigs  = [] 
  , gsDicts :: DEnv Var LocSpecType
gsDicts    = DEnv Var LocSpecType
dicts 
  , gsMethods :: [(Var, MethodType LocSpecType)]
gsMethods  = if Config -> Bool
noclasscheck Config
cfg then [] else DEnv Var LocSpecType
-> [DataConP] -> [CoreBind] -> [(Var, MethodType LocSpecType)]
Bare.makeMethodTypes DEnv Var LocSpecType
dicts (MeasEnv -> [DataConP]
Bare.meClasses  MeasEnv
measEnv) [CoreBind]
cbs 
  , gsInSigs :: [(Var, LocSpecType)]
gsInSigs   = [(Var, LocSpecType)]
forall a. Monoid a => a
mempty -- TODO-REBARE :: ![(Var, LocSpecType)]  
  , gsNewTypes :: [(TyCon, LocSpecType)]
gsNewTypes = Env -> SigEnv -> [(ModName, BareSpec)] -> [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, BareSpec)]
allSpecs 
  , gsTexprs :: [(Var, LocSpecType, [Located Expr])]
gsTexprs   = [ (Var
v, LocSpecType
t, [Located Expr]
es) | (Var
v, LocSpecType
t, Just [Located Expr]
es) <- [(Var, LocSpecType, Maybe [Located Expr])]
mySigs ] 
  }
  where 
    dicts :: DEnv Var LocSpecType
dicts      = Env -> SigEnv -> ModSpecs -> DEnv Var LocSpecType
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv ModSpecs
specs  
    mySpec :: BareSpec
mySpec     = BareSpec -> ModName -> ModSpecs -> BareSpec
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault BareSpec
forall a. Monoid a => a
mempty ModName
name ModSpecs
specs
    asmSigs :: [(Var, LocSpecType)]
asmSigs    = TycEnv -> [(Var, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv 
              [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ Env -> SigEnv -> ModName -> ModSpecs -> [(Var, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
name ModSpecs
specs 
              [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [ (Var
x,LocSpecType
t) | (ModName
_, Var
x, LocSpecType
t) <- [[(ModName, Var, LocSpecType)]] -> [(ModName, Var, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(ModName, Var, LocSpecType)]] -> [(ModName, Var, LocSpecType)])
-> [[(ModName, Var, LocSpecType)]] -> [(ModName, Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ ((Class, [(ModName, Var, LocSpecType)])
 -> [(ModName, Var, LocSpecType)])
-> [(Class, [(ModName, Var, LocSpecType)])]
-> [[(ModName, Var, LocSpecType)]]
forall a b. (a -> b) -> [a] -> [b]
map (Class, [(ModName, Var, LocSpecType)])
-> [(ModName, Var, LocSpecType)]
forall a b. (a, b) -> b
snd (MeasEnv -> [(Class, [(ModName, Var, LocSpecType)])]
Bare.meCLaws MeasEnv
measEnv)]
    tySigs :: [(Var, LocSpecType)]
tySigs     = [(Var, (Int, LocSpecType))] -> [(Var, LocSpecType)]
strengthenSigs ([(Var, (Int, LocSpecType))] -> [(Var, LocSpecType)])
-> ([[(Var, (Int, LocSpecType))]] -> [(Var, (Int, LocSpecType))])
-> [[(Var, (Int, LocSpecType))]]
-> [(Var, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Var, (Int, LocSpecType))]] -> [(Var, (Int, LocSpecType))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Var, (Int, LocSpecType))]] -> [(Var, LocSpecType)])
-> [[(Var, (Int, LocSpecType))]] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ 
                  [ [(Var
v, (Int
0, LocSpecType
t)) | (Var
v, LocSpecType
t,Maybe [Located Expr]
_) <- [(Var, LocSpecType, Maybe [Located Expr])]
mySigs                         ]   -- NOTE: these weights are to priortize 
                  , [(Var
v, (Int
1, LocSpecType
t)) | (Var
v, LocSpecType
t  ) <- MeasEnv -> [(Var, LocSpecType)]
makeMthSigs MeasEnv
measEnv            ]   -- user defined sigs OVER auto-generated 
                  , [(Var
v, (Int
2, LocSpecType
t)) | (Var
v, LocSpecType
t  ) <- Env -> BareRTEnv -> [(ModName, BareSpec)] -> [(Var, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, BareSpec)]
allSpecs ]   -- during the strengthening, i.e. to KEEP 
                  , [(Var
v, (Int
3, LocSpecType
t)) | (Var
v, LocSpecType
t  ) <- Env -> BareRTEnv -> [(ModName, BareSpec)] -> [(Var, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, BareSpec)]
allSpecs ]   -- the binders used in USER-defined sigs 
                  ]                                                               -- as they appear in termination metrics
    mySigs :: [(Var, LocSpecType, Maybe [Located Expr])]
mySigs     = FilePath
-> [(Var, LocSpecType, Maybe [Located Expr])]
-> [(Var, LocSpecType, Maybe [Located Expr])]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"MAKE-TYSIGS" ([(Var, LocSpecType, Maybe [Located Expr])]
 -> [(Var, LocSpecType, Maybe [Located Expr])])
-> [(Var, LocSpecType, Maybe [Located Expr])]
-> [(Var, LocSpecType, Maybe [Located Expr])]
forall a b. (a -> b) -> a -> b
$ Env
-> SigEnv
-> ModName
-> BareSpec
-> [(Var, LocSpecType, Maybe [Located Expr])]
makeTySigs  Env
env SigEnv
sigEnv ModName
name BareSpec
mySpec
    allSpecs :: [(ModName, BareSpec)]
allSpecs   = ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs 
    rtEnv :: BareRTEnv
rtEnv      = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv 
    -- hmeas      = makeHMeas    env allSpecs 

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

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

makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] 
makeInlSigs :: Env -> BareRTEnv -> [(ModName, BareSpec)] -> [(Var, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv 
  = BareRTEnv -> (Var -> RRType RReft) -> [Var] -> [(Var, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv Var -> RRType RReft
CoreToLogic.inlineSpecType 
  ([Var] -> [(Var, LocSpecType)])
-> ([(ModName, BareSpec)] -> [Var])
-> [(ModName, BareSpec)]
-> [(Var, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath
-> (BareSpec -> HashSet LocSymbol)
-> Env
-> [(ModName, BareSpec)]
-> [Var]
makeFromSet FilePath
"hinlines" BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Env
env 

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] 
makeMsrSigs :: Env -> BareRTEnv -> [(ModName, BareSpec)] -> [(Var, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv 
  = BareRTEnv -> (Var -> RRType RReft) -> [Var] -> [(Var, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv Var -> RRType RReft
CoreToLogic.measureSpecType 
  ([Var] -> [(Var, LocSpecType)])
-> ([(ModName, BareSpec)] -> [Var])
-> [(ModName, BareSpec)]
-> [(Var, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath
-> (BareSpec -> HashSet LocSymbol)
-> Env
-> [(ModName, BareSpec)]
-> [Var]
makeFromSet FilePath
"hmeas" BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Env
env 

makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
makeLiftedSigs :: BareRTEnv -> (Var -> RRType RReft) -> [Var] -> [(Var, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv Var -> RRType RReft
f [Var]
xs 
  = [(Var
x, LocSpecType
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 :: LocSpecType
lt = LocSpecType -> LocSpecType
expand (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ Located Var
lx {val :: RRType RReft
val = Var -> RRType RReft
f Var
x}
    ]
  where
    expand :: LocSpecType -> LocSpecType
expand   = BareRTEnv -> LocSpecType -> LocSpecType
Bare.specExpandType BareRTEnv
rtEnv 

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

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

bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> [(Ghc.Var, LocBareType)]
bareTySigs :: Env -> ModName -> BareSpec -> [(Var, LocBareType)]
bareTySigs Env
env ModName
name BareSpec
spec = [(Var, LocBareType)] -> [(Var, LocBareType)]
forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs 
  [ (Var
v, LocBareType
t) | (LocSymbol
x, LocBareType
t) <- BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs BareSpec
spec [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a. [a] -> [a] -> [a]
++ BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.localSigs BareSpec
spec  
           , let v :: Var
v   = FilePath -> Var -> Var
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"LOOKUP-GHC-VAR" (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"rawTySigs" LocSymbol
x 
  ] 

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


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

rawAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs :: Env -> ModName -> ModSpecs -> [(ModName, Var, LocBareType)]
rawAsmSigs Env
env ModName
myName ModSpecs
specs = 
  [ (ModName
m, Var
v, LocBareType
t) | (Var
v, [(Bool, ModName, LocBareType)]
sigs) <- Env
-> ModName -> ModSpecs -> [(Var, [(Bool, ModName, LocBareType)])]
allAsmSigs Env
env ModName
myName ModSpecs
specs 
              , let (ModName
m, LocBareType
t) = Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig Var
v [(Bool, ModName, LocBareType)]
sigs 
  ] 
    
myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig Var
v [(Bool, ModName, LocBareType)]
sigs = (ModName, LocBareType)
-> Maybe (ModName, LocBareType) -> (ModName, LocBareType)
forall a. a -> Maybe a -> a
Mb.fromMaybe (ModName, LocBareType)
forall a. a
errImp ([Maybe (ModName, LocBareType)] -> Maybe (ModName, LocBareType)
forall a. [Maybe a] -> Maybe a
Misc.firstMaybes [Maybe (ModName, LocBareType)
mbHome, Maybe (ModName, LocBareType)
mbImp]) 
  where 
    mbHome :: Maybe (ModName, LocBareType)
mbHome      = ([(ModName, LocBareType)] -> UserError)
-> [(ModName, LocBareType)] -> Maybe (ModName, LocBareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, LocBareType)] -> UserError
forall a a. [(a, Located a)] -> UserError
err                  [(ModName, LocBareType)]
sigsHome 
    mbImp :: Maybe (ModName, LocBareType)
mbImp       = ([(ModName, LocBareType)] -> UserError)
-> [(ModName, LocBareType)] -> Maybe (ModName, LocBareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, LocBareType)] -> UserError
forall a a. [(a, Located a)] -> UserError
err ([(Int, (ModName, LocBareType))] -> [(ModName, LocBareType)]
forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, LocBareType))]
sigsImp) -- see [NOTE:Prioritize-Home-Spec] 
    sigsHome :: [(ModName, LocBareType)]
sigsHome    = [(ModName
m, LocBareType
t)      | (Bool
True,  ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs ]
    sigsImp :: [(Int, (ModName, LocBareType))]
sigsImp     = FilePath
-> [(Int, (ModName, LocBareType))]
-> [(Int, (ModName, LocBareType))]
forall a. PPrint a => FilePath -> a -> a
F.notracepp (FilePath
"SIGS-IMP: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Var -> FilePath
forall a. PPrint a => a -> FilePath
F.showpp Var
v)
                  [(Int
d, (ModName
m, LocBareType
t)) | (Bool
False, ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
    err :: [(a, Located a)] -> UserError
err [(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 -> FilePath -> a
forall a. Maybe SrcSpan -> FilePath -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing FilePath
"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 -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec 
          -> [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
makeTExpr :: Env
-> ModName
-> [(Var, LocBareType)]
-> BareRTEnv
-> BareSpec
-> [(Var, LocBareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(Var, LocBareType)]
tySigs BareRTEnv
rtEnv BareSpec
spec 
                = FilePath
-> [(Var, LocBareType, Maybe [Located Expr])]
-> [(Var, LocBareType, Maybe [Located Expr])]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"MAKE-TEXPRS" 
                  [ (Var
v, LocBareType
t, LocBareType -> [Located Expr] -> [Located Expr]
forall (f :: * -> *).
Functor f =>
LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t ([Located Expr] -> [Located Expr])
-> Maybe [Located Expr] -> Maybe [Located Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Located Expr]
es) | (Var
v, (LocBareType
t, Maybe [Located Expr]
es)) <- HashMap Var (LocBareType, Maybe [Located Expr])
-> [(Var, (LocBareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Var (LocBareType, Maybe [Located Expr])
vSigExprs ] 
  where 
    qual :: LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t f (Located Expr)
es   = Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t (Located Expr -> Located Expr)
-> f (Located Expr) -> f (Located Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located Expr)
es
    vSigExprs :: HashMap Var (LocBareType, Maybe [Located Expr])
vSigExprs   = (Var -> LocBareType -> (LocBareType, Maybe [Located Expr]))
-> HashMap Var LocBareType
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\Var
v LocBareType
t -> (LocBareType
t, Var -> HashMap Var [Located Expr] -> Maybe [Located Expr]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
v HashMap Var [Located Expr]
vExprs)) HashMap Var LocBareType
vSigs 
    vExprs :: HashMap Var [Located Expr]
vExprs      = [(Var, [Located Expr])] -> HashMap Var [Located Expr]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (Env -> ModName -> BareSpec -> [(Var, [Located Expr])]
makeVarTExprs Env
env ModName
name BareSpec
spec) 
    vSigs :: HashMap Var LocBareType
vSigs       = [(Var, LocBareType)] -> HashMap Var LocBareType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Var, LocBareType)]
tySigs 
                    
qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr 
                -> Located F.Expr 
qualifyTermExpr :: Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t Located Expr
le 
        = Located Expr -> Expr -> Located Expr
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (Env
-> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
(Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs Expr
e)
  where 
    l :: SourcePos
l   = Located Expr -> SourcePos
forall a. Located a -> SourcePos
F.loc Located Expr
le 
    e :: Expr
e   = Located Expr -> Expr
forall a. Located a -> a
F.val Located Expr
le 
    bs :: [Symbol]
bs  = RTypeRep BTyCon BTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (RTypeRep BTyCon BTyVar RReft -> [Symbol])
-> (LocBareType -> RTypeRep BTyCon BTyVar RReft)
-> LocBareType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType BTyCon BTyVar RReft -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RType BTyCon BTyVar RReft -> RTypeRep BTyCon BTyVar RReft)
-> (LocBareType -> RType BTyCon BTyVar RReft)
-> LocBareType
-> RTypeRep BTyCon BTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocBareType -> RType BTyCon BTyVar RReft
forall a. Located a -> a
val (LocBareType -> [Symbol]) -> LocBareType -> [Symbol]
forall a b. (a -> b) -> a -> b
$ LocBareType
t 

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


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

allAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> [(Ghc.Var, [(Bool, ModName, LocBareType)])]
allAsmSigs :: Env
-> ModName -> ModSpecs -> [(Var, [(Bool, ModName, LocBareType)])]
allAsmSigs Env
env ModName
myName ModSpecs
specs = [(Var, (Bool, ModName, LocBareType))]
-> [(Var, [(Bool, ModName, LocBareType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList
  [ (Var
v, (Bool
must, ModName
name, LocBareType
t))  
      | (ModName
name, BareSpec
spec) <- ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs
      , (Bool
must, LocSymbol
x, LocBareType
t) <- ModName -> ModName -> BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs ModName
myName ModName
name BareSpec
spec
      , Var
v            <- Maybe Var -> [Var]
forall a. Maybe a -> [a]
Mb.maybeToList (Env -> ModName -> Bool -> LocSymbol -> Maybe Var
resolveAsmVar Env
env ModName
name Bool
must LocSymbol
x) 
  ] 

resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Maybe Ghc.Var 
resolveAsmVar :: Env -> ModName -> Bool -> LocSymbol -> Maybe Var
resolveAsmVar Env
env ModName
name Bool
True  LocSymbol
lx = Var -> Maybe Var
forall a. a -> Maybe a
Just (Var -> Maybe Var) -> Var -> Maybe Var
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> FilePath -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name FilePath
"resolveAsmVar-True"  LocSymbol
lx
resolveAsmVar Env
env ModName
name Bool
False LocSymbol
lx = Env -> ModName -> FilePath -> LocSymbol -> Maybe Var
forall a.
ResolveSym a =>
Env -> ModName -> FilePath -> LocSymbol -> Maybe a
Bare.maybeResolveSym     Env
env ModName
name FilePath
"resolveAsmVar-False" LocSymbol
lx  

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

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

makeSigEnv :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> S.HashSet StableName -> BareRTEnv -> Bare.SigEnv 
makeSigEnv :: TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv TCEmb TyCon
embs TyConMap
tyi HashSet StableName
exports BareRTEnv
rtEnv = SigEnv :: TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
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)] -> [(Ghc.TyCon, LocSpecType)]
makeNewTypes :: Env -> SigEnv -> [(ModName, BareSpec)] -> [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, BareSpec)]
specs = 
  [ (TyCon, LocSpecType)
ct | (ModName
name, BareSpec
spec) <- [(ModName, BareSpec)]
specs
       , DataDecl
d            <- BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.newtyDecls BareSpec
spec
       , (TyCon, LocSpecType)
ct           <- Env -> SigEnv -> ModName -> DataDecl -> [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv ModName
name DataDecl
d 
  ] 

makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl -> [(Ghc.TyCon, LocSpecType)]
makeNewType :: Env -> SigEnv -> ModName -> DataDecl -> [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv ModName
name DataDecl
d 
 | Just TyCon
tc <- Maybe TyCon
tcMb            = [(TyCon
tc, LocSpecType
t)] 
 | Bool
otherwise                  = []
  where 
    tcMb :: Maybe TyCon
tcMb                      = Env -> ModName -> FilePath -> DataName -> Maybe TyCon
Bare.lookupGhcDnTyCon Env
env ModName
name FilePath
"makeNewType" DataName
tcName
    tcName :: DataName
tcName                    = DataDecl -> DataName
tycName DataDecl
d
    t :: LocSpecType
t                         = Env
-> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV LocBareType
bt
    bt :: LocBareType
bt                        = DataName -> SourcePos -> [DataCtor] -> LocBareType
forall a. PPrint a => a -> SourcePos -> [DataCtor] -> LocBareType
getTy DataName
tcName (DataDecl -> SourcePos
tycSrcPos DataDecl
d) (DataDecl -> [DataCtor]
tycDCons DataDecl
d)
    getTy :: a -> SourcePos -> [DataCtor] -> LocBareType
getTy a
_ SourcePos
l [DataCtor
c]
      | [(Symbol
_, RType BTyCon BTyVar RReft
t)] <- DataCtor -> [(Symbol, RType BTyCon BTyVar RReft)]
dcFields DataCtor
c = SourcePos -> SourcePos -> RType BTyCon BTyVar RReft -> LocBareType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l RType BTyCon BTyVar RReft
t
    getTy a
n SourcePos
l [DataCtor]
_                = UserError -> LocBareType
forall a e. Exception e => e -> a
Ex.throw (a -> SourcePos -> UserError
forall a. PPrint a => a -> SourcePos -> UserError
err a
n SourcePos
l) 
    err :: a -> SourcePos -> UserError
err 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
-> ModSpecs
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig ModSpecs
specs = SpData :: [(Var, LocSpecType)]
-> [(Symbol, LocSpecType)]
-> [(Maybe Var, LocSpecType)]
-> [(LocSpecType, LocSpecType)]
-> [Measure (RRType RReft) DataCon]
-> [UnSortedExpr]
-> GhcSpecData
SpData 
  { gsCtors :: [(Var, LocSpecType)]
gsCtors      = -- F.notracepp "GS-CTORS" 
                   [ (Var
x, LocSpecType
tt) 
                       | (Var
x, LocSpecType
t) <- MeasEnv -> [(Var, LocSpecType)]
Bare.meDataCons MeasEnv
measEnv
                       , let tt :: LocSpecType
tt  = SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
Bare.plugHoles SigEnv
sigEnv ModName
name (Var -> PlugTV Var
forall v. v -> PlugTV v
Bare.LqTV Var
x) LocSpecType
t 
                   ]
  , gsMeas :: [(Symbol, LocSpecType)]
gsMeas       = [ (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, RRType Reft -> RRType RReft
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RRType Reft -> RRType RReft)
-> Located (RRType Reft) -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (RRType Reft)
t) | (Symbol
x, Located (RRType Reft)
t) <- [(Symbol, Located (RRType Reft))]
measVars ] 
  , gsMeasures :: [Measure (RRType RReft) DataCon]
gsMeasures   = Env
-> ModName
-> Measure (RRType RReft) DataCon
-> Measure (RRType RReft) DataCon
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (Measure (RRType RReft) DataCon -> Measure (RRType RReft) DataCon)
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Measure (RRType RReft) DataCon]
ms1 [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall a. [a] -> [a] -> [a]
++ [Measure (RRType RReft) DataCon]
ms2)
  , gsInvariants :: [(Maybe Var, LocSpecType)]
gsInvariants = ((Maybe Var, LocSpecType) -> SourcePos)
-> [(Maybe Var, LocSpecType)] -> [(Maybe Var, LocSpecType)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc (LocSpecType -> SourcePos)
-> ((Maybe Var, LocSpecType) -> LocSpecType)
-> (Maybe Var, LocSpecType)
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Var, LocSpecType) -> LocSpecType
forall a b. (a, b) -> b
snd) [(Maybe Var, LocSpecType)]
invs 
  , gsIaliases :: [(LocSpecType, LocSpecType)]
gsIaliases   = ((ModName, BareSpec) -> [(LocSpecType, LocSpecType)])
-> [(ModName, BareSpec)] -> [(LocSpecType, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv -> (ModName, BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv) (ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs)
  , gsUnsorted :: [UnSortedExpr]
gsUnsorted   = [UnSortedExpr]
usI [UnSortedExpr] -> [UnSortedExpr] -> [UnSortedExpr]
forall a. [a] -> [a] -> [a]
++ ((Measure LocBareType LocSymbol -> [UnSortedExpr])
-> [Measure LocBareType LocSymbol] -> [UnSortedExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure LocBareType LocSymbol -> [UnSortedExpr]
forall ty ctor. Measure ty ctor -> [UnSortedExpr]
msUnSorted ([Measure LocBareType LocSymbol] -> [UnSortedExpr])
-> [Measure LocBareType LocSymbol] -> [UnSortedExpr]
forall a b. (a -> b) -> a -> b
$ (BareSpec -> [Measure LocBareType LocSymbol])
-> ModSpecs -> [Measure LocBareType LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures ModSpecs
specs)
  }
  where
    measVars :: [(Symbol, Located (RRType Reft))]
measVars     = MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms      MeasEnv
measEnv -- ms'
                [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv -- cms' 
                [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ Env -> [(Symbol, Located (RRType Reft))]
forall r. Monoid r => Env -> [(Symbol, Located (RRType r))]
Bare.varMeasures Env
env
    measuresSp :: MSpec (RRType RReft) DataCon
measuresSp   = MeasEnv -> MSpec (RRType RReft) DataCon
Bare.meMeasureSpec MeasEnv
measEnv  
    ms1 :: [Measure (RRType RReft) DataCon]
ms1          = HashMap LocSymbol (Measure (RRType RReft) DataCon)
-> [Measure (RRType RReft) DataCon]
forall k v. HashMap k v -> [v]
M.elems (MSpec (RRType RReft) DataCon
-> HashMap LocSymbol (Measure (RRType RReft) DataCon)
forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
Ms.measMap MSpec (RRType RReft) DataCon
measuresSp)
    ms2 :: [Measure (RRType RReft) DataCon]
ms2          =          MSpec (RRType RReft) DataCon -> [Measure (RRType RReft) DataCon]
forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
Ms.imeas   MSpec (RRType RReft) DataCon
measuresSp
    mySpec :: BareSpec
mySpec       = BareSpec -> ModName -> ModSpecs -> BareSpec
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault BareSpec
forall a. Monoid a => a
mempty ModName
name ModSpecs
specs
    name :: ModName
name         = GhcSrc -> ModName
_giTargetMod      GhcSrc
src
    ([(Maybe Var, LocSpecType)]
minvs,[UnSortedExpr]
usI)  = Env
-> ModName
-> GhcSpecSig
-> BareSpec
-> ([(Maybe Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig BareSpec
mySpec
    invs :: [(Maybe Var, LocSpecType)]
invs         = [(Maybe Var, LocSpecType)]
minvs [(Maybe Var, LocSpecType)]
-> [(Maybe Var, LocSpecType)] -> [(Maybe Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [[(Maybe Var, LocSpecType)]] -> [(Maybe Var, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Env -> SigEnv -> (ModName, BareSpec) -> [(Maybe Var, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv ((ModName, BareSpec) -> [(Maybe Var, LocSpecType)])
-> [(ModName, BareSpec)] -> [[(Maybe Var, LocSpecType)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs)

makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases :: Env
-> SigEnv -> (ModName, BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv (ModName
name, BareSpec
spec)
  = [ (LocSpecType, LocSpecType)
z | Right (LocSpecType, LocSpecType)
z <- (LocBareType, LocBareType)
-> Either UserError (LocSpecType, LocSpecType)
mkIA ((LocBareType, LocBareType)
 -> Either UserError (LocSpecType, LocSpecType))
-> [(LocBareType, LocBareType)]
-> [Either UserError (LocSpecType, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [(LocBareType, LocBareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
Ms.ialiases BareSpec
spec ]
  where 
    -- mkIA :: (LocBareType, LocBareType) -> Either _ (LocSpecType, LocSpecType)
    mkIA :: (LocBareType, LocBareType)
-> Either UserError (LocSpecType, LocSpecType)
mkIA (LocBareType
t1, LocBareType
t2) = (,) (LocSpecType -> LocSpecType -> (LocSpecType, LocSpecType))
-> Either UserError LocSpecType
-> Either UserError (LocSpecType -> (LocSpecType, LocSpecType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocBareType -> Either UserError LocSpecType
mkI LocBareType
t1 Either UserError (LocSpecType -> (LocSpecType, LocSpecType))
-> Either UserError LocSpecType
-> Either UserError (LocSpecType, LocSpecType)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LocBareType -> Either UserError LocSpecType
mkI LocBareType
t2
    mkI :: LocBareType -> Either UserError LocSpecType
mkI           = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Either UserError LocSpecType
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, BareSpec) -> [(Maybe Var, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv (ModName
name, BareSpec
spec) = 
  [ (Maybe Var
forall a. Maybe a
Nothing, LocSpecType
t) 
    | (Maybe LocSymbol
_, LocBareType
bt) <- BareSpec -> [(Maybe LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
Ms.invariants BareSpec
spec 
    , Env -> ModName -> LocBareType -> Bool
Bare.knownGhcType Env
env ModName
name LocBareType
bt
    , let t :: LocSpecType
t = Env
-> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV LocBareType
bt
  ]

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

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

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

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


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


-- REBARE: formerly, makeGhcSpec3
-------------------------------------------------------------------------------------------
makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
-------------------------------------------------------------------------------------------
makeSpecName :: Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env TycEnv
tycEnv MeasEnv
measEnv ModName
name = SpNames :: [(Symbol, Var)]
-> [Located DataCon]
-> [TyConP]
-> TCEmb TyCon
-> [DataDecl]
-> TyConMap
-> GhcSpecNames
SpNames 
  { gsFreeSyms :: [(Symbol, Var)]
gsFreeSyms = Env -> [(Symbol, Var)]
Bare.reSyms Env
env 
  , gsDconsP :: [Located DataCon]
gsDconsP   = [ DataConP -> DataCon -> Located DataCon
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ] 
  , gsTconsP :: [TyConP]
gsTconsP   = Env -> ModName -> TyConP -> TyConP
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (TyConP -> TyConP) -> [TyConP] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyConP]
tycons                
  -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
  , gsTcEmbeds :: TCEmb TyCon
gsTcEmbeds = TycEnv -> TCEmb TyCon
Bare.tcEmbs     TycEnv
tycEnv   
  , gsADTs :: [DataDecl]
gsADTs     = TycEnv -> [DataDecl]
Bare.tcAdts     TycEnv
tycEnv 
  , gsTyconEnv :: TyConMap
gsTyconEnv = TycEnv -> TyConMap
Bare.tcTyConMap TycEnv
tycEnv  
  }
  where 
    datacons, cls :: [DataConP]
    datacons :: [DataConP]
datacons   = TycEnv -> [DataConP]
Bare.tcDataCons TycEnv
tycEnv 
    cls :: [DataConP]
cls        = FilePath -> [DataConP] -> [DataConP]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"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
-------------------------------------------------------------------------------------------
makeTycEnv :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs 
           -> Bare.TycEnv 
-------------------------------------------------------------------------------------------
makeTycEnv :: Config
-> ModName -> Env -> TCEmb TyCon -> BareSpec -> ModSpecs -> TycEnv
makeTycEnv Config
cfg ModName
myName Env
env TCEmb TyCon
embs BareSpec
mySpec ModSpecs
iSpecs = TycEnv :: [TyConP]
-> [DataConP]
-> [Measure (RRType RReft) DataCon]
-> [(Var, LocSpecType)]
-> TyConMap
-> [DataDecl]
-> DataConMap
-> TCEmb TyCon
-> ModName
-> TycEnv
Bare.TycEnv 
  { tcTyCons :: [TyConP]
tcTyCons      = [TyConP]
tycons                  
  , tcDataCons :: [DataConP]
tcDataCons    = 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 
  , tcSelMeasures :: [Measure (RRType RReft) DataCon]
tcSelMeasures = [Measure (RRType RReft) DataCon]
dcSelectors             
  , tcSelVars :: [(Var, LocSpecType)]
tcSelVars     = [(Var, LocSpecType)]
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]])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. [([a], [b])] -> ([a], [b])
Misc.concatUnzip ([([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
 -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> [([(ModName, TyConP, Maybe DataPropDecl)],
     [[Located DataConP]])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. (a -> b) -> a -> b
$ Env
-> (ModName, BareSpec)
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes Env
env ((ModName, BareSpec)
 -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> [(ModName, BareSpec)]
-> [([(ModName, TyConP, Maybe DataPropDecl)],
     [[Located DataConP]])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, BareSpec)]
specs 
    specs :: [(ModName, BareSpec)]
specs         = (ModName
myName, BareSpec
mySpec) (ModName, BareSpec)
-> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
forall a. a -> [a] -> [a]
: ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
iSpecs
    tcs :: [TyConP]
tcs           = (ModName, TyConP, Maybe DataPropDecl) -> TyConP
forall a b c. (a, b, c) -> b
Misc.snd3 ((ModName, TyConP, Maybe DataPropDecl) -> TyConP)
-> [(ModName, TyConP, Maybe DataPropDecl)] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds 
    tyi :: TyConMap
tyi           = Env -> ModName -> TyConMap -> TyConMap
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
myName (TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
embs [TyCon]
fiTcs [TyConP]
tycons)
    -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
    -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
    tycons :: [TyConP]
tycons        = [TyConP]
tcs [TyConP] -> [TyConP] -> [TyConP]
forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
myName 
    datacons :: [Located DataConP]
datacons      = TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
Bare.makePluggedDataCon TCEmb TyCon
embs TyConMap
tyi (Located DataConP -> Located DataConP)
-> [Located DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Located DataConP]] -> [Located DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs [Located DataConP] -> [Located DataConP] -> [Located DataConP]
forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
myName)
    tds :: [(ModName, TyCon, DataPropDecl)]
tds           = [(ModName
name, TyConP -> TyCon
tcpCon TyConP
tcp, DataPropDecl
dd) | (ModName
name, TyConP
tcp, Just DataPropDecl
dd) <- [(ModName, TyConP, Maybe DataPropDecl)]
tcDds]
    adts :: [DataDecl]
adts          = Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> [DataDecl]
Bare.makeDataDecls Config
cfg TCEmb TyCon
embs ModName
myName [(ModName, TyCon, DataPropDecl)]
tds       [Located DataConP]
datacons
    dm :: DataConMap
dm            = [DataDecl] -> DataConMap
Bare.dataConMap [DataDecl]
adts
    dcSelectors :: [Measure (RRType RReft) DataCon]
dcSelectors   = (Located DataConP -> [Measure (RRType RReft) DataCon])
-> [Located DataConP] -> [Measure (RRType RReft) DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Config
-> DataConMap
-> Located DataConP
-> [Measure (RRType RReft) DataCon]
Bare.makeMeasureSelectors Config
cfg DataConMap
dm) [Located DataConP]
datacons
    recSelectors :: [(Var, LocSpecType)]
recSelectors  = Env -> ModName -> [Located DataConP] -> [(Var, LocSpecType)]
Bare.makeRecordSelectorSigs Env
env ModName
myName       [Located DataConP]
datacons
    fiTcs :: [TyCon]
fiTcs         = GhcSrc -> [TyCon]
_gsFiTcs (Env -> GhcSrc
Bare.reSrc Env
env)
   
knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP] 
knownWiredDataCons :: Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
name = (Located DataConP -> Bool)
-> [Located DataConP] -> [Located DataConP]
forall a. (a -> Bool) -> [a] -> [a]
filter Located DataConP -> Bool
isKnown [Located DataConP]
wiredDataCons 
  where 
    isKnown :: Located DataConP -> Bool
isKnown                 = Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcDataCon Env
env ModName
name (LocSymbol -> Bool)
-> (Located DataConP -> LocSymbol) -> Located DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (DataCon -> LocSymbol)
-> (Located DataConP -> DataCon) -> Located DataConP -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
val

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


-- REBARE: formerly, makeGhcCHOP2
-------------------------------------------------------------------------------------------
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs -> Bare.MeasEnv 
-------------------------------------------------------------------------------------------
makeMeasEnv :: Env -> TycEnv -> SigEnv -> ModSpecs -> MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv ModSpecs
specs = MeasEnv :: MSpec (RRType RReft) DataCon
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Var, LocSpecType)]
-> [DataConP]
-> [(ModName, Var, LocSpecType)]
-> [(Class, [(ModName, Var, LocSpecType)])]
-> MeasEnv
Bare.MeasEnv 
  { meMeasureSpec :: MSpec (RRType RReft) DataCon
meMeasureSpec = MSpec (RRType RReft) DataCon
measures 
  , meClassSyms :: [(Symbol, Located (RRType Reft))]
meClassSyms   = [(Symbol, Located (RRType Reft))]
cms' 
  , meSyms :: [(Symbol, Located (RRType Reft))]
meSyms        = [(Symbol, Located (RRType Reft))]
ms' 
  , meDataCons :: [(Var, LocSpecType)]
meDataCons    = [(Var, LocSpecType)]
cs' 
  , meClasses :: [DataConP]
meClasses     = [DataConP]
cls
  , meMethods :: [(ModName, Var, LocSpecType)]
meMethods     = [(ModName, Var, LocSpecType)]
mts [(ModName, Var, LocSpecType)]
-> [(ModName, Var, LocSpecType)] -> [(ModName, Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(ModName, Var, LocSpecType)]
dms 
  , meCLaws :: [(Class, [(ModName, Var, LocSpecType)])]
meCLaws       = [(Class, [(ModName, Var, LocSpecType)])]
laws
  }
  where 
    measures :: MSpec (RRType RReft) DataCon
measures      = [MSpec (RRType RReft) DataCon] -> MSpec (RRType RReft) DataCon
forall a. Monoid a => [a] -> a
mconcat ([Measure (RRType RReft) DataCon] -> MSpec (RRType RReft) DataCon
forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
Ms.mkMSpec' [Measure (RRType RReft) DataCon]
dcSelectors MSpec (RRType RReft) DataCon
-> [MSpec (RRType RReft) DataCon] -> [MSpec (RRType RReft) DataCon]
forall a. a -> [a] -> [a]
: (Env
-> SigEnv
-> ModName
-> (ModName, BareSpec)
-> MSpec (RRType RReft) DataCon
Bare.makeMeasureSpec Env
env SigEnv
sigEnv ModName
name ((ModName, BareSpec) -> MSpec (RRType RReft) DataCon)
-> [(ModName, BareSpec)] -> [MSpec (RRType RReft) DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs))
    ([(Var, RRType RReft)]
cs, [(LocSymbol, RRType Reft)]
ms)      = MSpec (RRType RReft) DataCon
-> ([(Var, RRType RReft)], [(LocSymbol, RRType Reft)])
Bare.makeMeasureSpec'     MSpec (RRType RReft) DataCon
measures
    cms :: [(LocSymbol, CMeasure (RRType Reft))]
cms           = MSpec (RRType RReft) DataCon
-> [(LocSymbol, CMeasure (RRType Reft))]
forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
Bare.makeClassMeasureSpec MSpec (RRType RReft) DataCon
measures
    cms' :: [(Symbol, Located (RRType Reft))]
cms'          = [ (Symbol
x, SourcePos -> SourcePos -> RRType Reft -> Located (RRType Reft)
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (RRType Reft -> Located (RRType Reft))
-> RRType Reft -> Located (RRType Reft)
forall a b. (a -> b) -> a -> b
$ CMeasure (RRType Reft) -> RRType Reft
forall ty. CMeasure ty -> ty
cSort CMeasure (RRType Reft)
t)  | (Loc SourcePos
l SourcePos
l' Symbol
x, CMeasure (RRType Reft)
t) <- [(LocSymbol, CMeasure (RRType Reft))]
cms ]
    ms' :: [(Symbol, Located (RRType Reft))]
ms'           = [ (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, LocSymbol -> RRType Reft -> Located (RRType Reft)
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lx RRType Reft
t) | (LocSymbol
lx, RRType Reft
t) <- [(LocSymbol, RRType Reft)]
ms
                                               , Maybe (Located (RRType Reft)) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Symbol
-> [(Symbol, Located (RRType Reft))]
-> Maybe (Located (RRType Reft))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx) [(Symbol, Located (RRType Reft))]
cms') ]
    cs' :: [(Var, LocSpecType)]
cs'           = [ (Var
v, Var -> RRType RReft -> LocSpecType
forall b. NamedThing b => b -> RRType RReft -> LocSpecType
txRefs Var
v RRType RReft
t) | (Var
v, RRType RReft
t) <- TCEmb TyCon
-> [(Var, RRType RReft)] -> [DataConP] -> [(Var, RRType RReft)]
Bare.meetDataConSpec TCEmb TyCon
embs [(Var, RRType RReft)]
cs ([DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
    txRefs :: b -> RRType RReft -> LocSpecType
txRefs b
v RRType RReft
t    = TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (RRType RReft -> b -> RRType RReft
forall a b. a -> b -> a
const RRType RReft
t (b -> RRType RReft) -> Located b -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Located b
forall a. NamedThing a => a -> Located a
GM.locNamedThing b
v) 
    -- unpacking the environment
    tyi :: TyConMap
tyi           = TycEnv -> TyConMap
Bare.tcTyConMap    TycEnv
tycEnv 
    dcSelectors :: [Measure (RRType RReft) DataCon]
dcSelectors   = TycEnv -> [Measure (RRType RReft) 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
    dms :: [(ModName, Var, LocSpecType)]
dms           = Env
-> [(ModName, Var, LocSpecType)] -> [(ModName, Var, LocSpecType)]
Bare.makeDefaultMethods Env
env [(ModName, Var, LocSpecType)]
mts  
    ([DataConP]
cls, [(ModName, Var, LocSpecType)]
mts)    = Env
-> SigEnv
-> ModName
-> ModSpecs
-> ([DataConP], [(ModName, Var, LocSpecType)])
Bare.makeClasses        Env
env SigEnv
sigEnv ModName
name ModSpecs
specs
    laws :: [(Class, [(ModName, Var, LocSpecType)])]
laws          = Env
-> SigEnv
-> ModName
-> ModSpecs
-> [(Class, [(ModName, Var, LocSpecType)])]
Bare.makeCLaws Env
env SigEnv
sigEnv ModName
name ModSpecs
specs

-----------------------------------------------------------------------------------------
-- | @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 :: GhcSrc -> Bare.Env 
               -> GhcSpecRefl -> GhcSpecData -> GhcSpecSig -> GhcSpecQual -> BareRTEnv 
               -> Ms.BareSpec -> Ms.BareSpec 
-----------------------------------------------------------------------------------------
makeLiftedSpec :: GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> BareSpec
-> BareSpec
makeLiftedSpec GhcSrc
src Env
_env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE BareSpec
lSpec0 = BareSpec
lSpec0 
  { asmSigs :: [(LocSymbol, LocBareType)]
Ms.asmSigs    = FilePath
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a. PPrint a => FilePath -> a -> a
F.notracepp   FilePath
"LIFTED-ASM-SIGS" ([(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)])
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ [(LocSymbol, LocBareType)]
xbs -- ++ mkSigs (gsAsmSigs sig)
  , reflSigs :: [(LocSymbol, LocBareType)]
Ms.reflSigs   = FilePath
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"REFL-SIGS"         [(LocSymbol, LocBareType)]
xbs
  , sigs :: [(LocSymbol, LocBareType)]
Ms.sigs       = FilePath
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a. PPrint a => FilePath -> a -> a
F.notracepp   FilePath
"LIFTED-SIGS"     ([(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)])
-> [(LocSymbol, LocBareType)] -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$        [(Var, LocSpecType)] -> [(LocSymbol, LocBareType)]
forall (f :: * -> *).
Functor f =>
[(Var, f (RRType RReft))]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sig)  
  , invariants :: [(Maybe LocSymbol, LocBareType)]
Ms.invariants = [ ((Var -> LocSymbol
varLocSym (Var -> LocSymbol) -> Maybe Var -> Maybe LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Var
x), RRType RReft -> RType BTyCon BTyVar RReft
Bare.specToBare (RRType RReft -> RType BTyCon BTyVar RReft)
-> LocSpecType -> LocBareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSpecType
t) 
                       | (Maybe Var
x, LocSpecType
t) <- GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants GhcSpecData
sData 
                       , FilePath -> LocSpecType -> Bool
forall a. Loc a => FilePath -> a -> Bool
isLocInFile FilePath
srcF LocSpecType
t
                    ]
  , axeqs :: [Equation]
Ms.axeqs      = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
refl 
  , aliases :: [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
Ms.aliases    = FilePath
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
forall a. PPrint a => FilePath -> a -> a
F.notracepp FilePath
"MY-ALIASES" ([Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
 -> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))])
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
forall a b. (a -> b) -> a -> b
$ HashMap
  Symbol (Located (RTAlias Symbol (RType BTyCon BTyVar RReft)))
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
forall k v. HashMap k v -> [v]
M.elems (HashMap
   Symbol (Located (RTAlias Symbol (RType BTyCon BTyVar RReft)))
 -> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))])
-> (BareRTEnv
    -> HashMap
         Symbol (Located (RTAlias Symbol (RType BTyCon BTyVar RReft))))
-> BareRTEnv
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv
-> HashMap
     Symbol (Located (RTAlias Symbol (RType BTyCon BTyVar RReft)))
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases (BareRTEnv
 -> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))])
-> BareRTEnv
-> [Located (RTAlias Symbol (RType BTyCon BTyVar RReft))]
forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE
  , ealiases :: [Located (RTAlias Symbol Expr)]
Ms.ealiases   = HashMap Symbol (Located (RTAlias Symbol Expr))
-> [Located (RTAlias Symbol Expr)]
forall k v. HashMap k v -> [v]
M.elems (HashMap Symbol (Located (RTAlias Symbol Expr))
 -> [Located (RTAlias Symbol Expr)])
-> (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr)))
-> BareRTEnv
-> [Located (RTAlias Symbol Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases (BareRTEnv -> [Located (RTAlias Symbol Expr)])
-> BareRTEnv -> [Located (RTAlias Symbol Expr)]
forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE 
  , qualifiers :: [Qualifier]
Ms.qualifiers = (Qualifier -> Bool) -> [Qualifier] -> [Qualifier]
forall a. (a -> Bool) -> [a] -> [a]
filter (FilePath -> Qualifier -> Bool
forall a. Loc a => FilePath -> a -> Bool
isLocInFile FilePath
srcF) (GhcSpecQual -> [Qualifier]
gsQualifiers GhcSpecQual
qual)
  }
  where
    mkSigs :: [(Var, f (RRType RReft))]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs [(Var, f (RRType RReft))]
xts    = [ (Var, f (RRType RReft))
-> (LocSymbol, f (RType BTyCon BTyVar RReft))
forall (f :: * -> *).
Functor f =>
(Var, f (RRType RReft))
-> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare (Var
x, f (RRType RReft)
t) | (Var
x, f (RRType RReft)
t) <- [(Var, f (RRType RReft))]
xts
                    ,  Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x HashSet Var
sigVars Bool -> Bool -> Bool
&& (TargetSrc -> Var -> Bool
isExportedVar (Optic' An_Iso NoIx GhcSrc TargetSrc -> GhcSrc -> TargetSrc
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' An_Iso NoIx GhcSrc TargetSrc
targetSrcIso GhcSrc
src) Var
x) 
                    ] 
    toBare :: (Var, f (RRType RReft))
-> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare (Var
x, f (RRType RReft)
t) = (Var -> LocSymbol
varLocSym Var
x, RRType RReft -> RType BTyCon BTyVar RReft
Bare.specToBare (RRType RReft -> RType BTyCon BTyVar RReft)
-> f (RRType RReft) -> f (RType BTyCon BTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (RRType RReft)
t)
    xbs :: [(LocSymbol, LocBareType)]
xbs           = (Var, LocSpecType) -> (LocSymbol, LocBareType)
forall (f :: * -> *).
Functor f =>
(Var, f (RRType RReft))
-> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare ((Var, LocSpecType) -> (LocSymbol, LocBareType))
-> [(Var, LocSpecType)] -> [(LocSymbol, LocBareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, LocSpecType)]
reflTySigs 
    sigVars :: HashSet Var
sigVars       = HashSet Var -> HashSet Var -> HashSet Var
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet Var
defVars HashSet Var
reflVars
    defVars :: HashSet Var
defVars       = [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (GhcSrc -> [Var]
_giDefVars GhcSrc
src)
    reflTySigs :: [(Var, LocSpecType)]
reflTySigs    = [(Var
x, LocSpecType
t) | (Var
x,LocSpecType
t,Equation
_) <- GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl, Var
x Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
refl]
    reflVars :: HashSet Var
reflVars      = [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, LocSpecType) -> Var) -> [(Var, LocSpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, LocSpecType)]
reflTySigs)
    -- myAliases fld = M.elems . fld $ myRTE 
    srcF :: FilePath
srcF          = GhcSrc -> FilePath
_giTarget GhcSrc
src 

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

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

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

varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: Var -> LocSymbol
varLocSym Var
v = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Located Var -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Located Var
forall a. NamedThing a => a -> Located a
GM.locNamedThing Var
v

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


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

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

    fixArg  :: Symbol -> Symbol 
    fixArg :: Symbol -> Symbol
fixArg  = 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 
      
    fixBody :: BareType -> BareType 
    fixBody :: RType BTyCon BTyVar RReft -> RType BTyCon BTyVar RReft
fixBody = RRType RReft -> RType BTyCon BTyVar RReft
Bare.specToBare 
            (RRType RReft -> RType BTyCon BTyVar RReft)
-> (RType BTyCon BTyVar RReft -> RRType RReft)
-> RType BTyCon BTyVar RReft
-> RType BTyCon BTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> RRType RReft
forall a. Located a -> a
F.val 
            (LocSpecType -> RRType RReft)
-> (RType BTyCon BTyVar RReft -> LocSpecType)
-> RType BTyCon BTyVar RReft
-> RRType RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.RawTV 
            (LocBareType -> LocSpecType)
-> (RType BTyCon BTyVar RReft -> LocBareType)
-> RType BTyCon BTyVar RReft
-> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (RType BTyCon BTyVar RReft))
-> RType BTyCon BTyVar RReft -> LocBareType
forall l b. Loc l => l -> b -> Located b
F.atLoc Located (RTAlias Symbol (RType BTyCon BTyVar RReft))
lx